rusub_5.miz



    begin

    definition

      let V be non empty RLSStruct, M,N be Affine Subset of V;

      :: RUSUB_5:def1

      pred M is_parallel_to N means ex v be VECTOR of V st M = (N + {v});

    end

    theorem :: RUSUB_5:1

    for V be right_zeroed non empty RLSStruct, M be Affine Subset of V holds M is_parallel_to M

    proof

      let V be right_zeroed non empty RLSStruct;

      let M be Affine Subset of V;

      take ( 0. V);

      for x be object st x in (M + {( 0. V)}) holds x in M

      proof

        let x be object;

        assume x in (M + {( 0. V)});

        then x in { (u + v) where u,v be Element of V : u in M & v in {( 0. V)} } by RUSUB_4:def 9;

        then

        consider u,v be Element of V such that

         A1: x = (u + v) & u in M and

         A2: v in {( 0. V)};

        v = ( 0. V) by A2, TARSKI:def 1;

        hence thesis by A1, RLVECT_1:def 4;

      end;

      then

       A3: (M + {( 0. V)}) c= M;

      for x be object st x in M holds x in (M + {( 0. V)})

      proof

        let x be object;

        assume

         A4: x in M;

        then

        reconsider x as Element of V;

        x = (x + ( 0. V)) & ( 0. V) in {( 0. V)} by RLVECT_1:def 4, TARSKI:def 1;

        then x in { (u + v) where u,v be Element of V : u in M & v in {( 0. V)} } by A4;

        hence thesis by RUSUB_4:def 9;

      end;

      then M c= (M + {( 0. V)});

      hence thesis by A3;

    end;

    theorem :: RUSUB_5:2

    

     Th2: for V be add-associative right_zeroed right_complementable non empty RLSStruct, M,N be Affine Subset of V st M is_parallel_to N holds N is_parallel_to M

    proof

      let V be add-associative right_zeroed right_complementable non empty RLSStruct;

      let M,N be Affine Subset of V;

      assume M is_parallel_to N;

      then

      consider w1 be VECTOR of V such that

       A1: M = (N + {w1});

      set w2 = ( - w1);

      for x be object st x in N holds x in (M + {w2})

      proof

        let x be object;

        assume

         A2: x in N;

        then

        reconsider x as Element of V;

        set y = (x + w1);

        w1 in {w1} by TARSKI:def 1;

        then y in { (u + v) where u,v be Element of V : u in N & v in {w1} } by A2;

        then

         A3: y in M by A1, RUSUB_4:def 9;

        (x + (w1 + w2)) = (y + w2) by RLVECT_1:def 3;

        then (x + ( 0. V)) = (y + w2) by RLVECT_1: 5;

        then

         A4: x = (y + w2);

        w2 in {w2} by TARSKI:def 1;

        then x in { (u + v) where u,v be Element of V : u in M & v in {w2} } by A3, A4;

        hence thesis by RUSUB_4:def 9;

      end;

      then

       A5: N c= (M + {w2});

      take w2;

      for x be object st x in (M + {w2}) holds x in N

      proof

        let x be object;

        assume

         A6: x in (M + {w2});

        then x in { (u + v) where u,v be Element of V : u in M & v in {w2} } by RUSUB_4:def 9;

        then

        consider u9,v9 be Element of V such that

         A7: x = (u9 + v9) and

         A8: u9 in M and

         A9: v9 in {w2};

        reconsider x as Element of V by A6;

        x = (u9 + w2) by A7, A9, TARSKI:def 1;

        then (x + w1) = (u9 + (w2 + w1)) by RLVECT_1:def 3;

        then

         A10: (x + w1) = (u9 + ( 0. V)) by RLVECT_1: 5;

        u9 in { (u + v) where u,v be Element of V : u in N & v in {w1} } by A1, A8, RUSUB_4:def 9;

        then

        consider u1,v1 be Element of V such that

         A11: u9 = (u1 + v1) & u1 in N and

         A12: v1 in {w1};

        w1 = v1 by A12, TARSKI:def 1;

        hence thesis by A10, A11, RLVECT_1: 8;

      end;

      then (M + {w2}) c= N;

      hence thesis by A5;

    end;

    theorem :: RUSUB_5:3

    

     Th3: for V be Abelian add-associative right_zeroed right_complementable non empty RLSStruct, M,L,N be Affine Subset of V st M is_parallel_to L & L is_parallel_to N holds M is_parallel_to N

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty RLSStruct;

      let M,L,N be Affine Subset of V;

      assume that

       A1: M is_parallel_to L and

       A2: L is_parallel_to N;

      consider v1 be Element of V such that

       A3: M = (L + {v1}) by A1;

      consider u1 be Element of V such that

       A4: L = (N + {u1}) by A2;

      set w = (u1 + v1);

      for x be object st x in (N + {w}) holds x in M

      proof

        let x be object;

        

         A5: u1 in {u1} by TARSKI:def 1;

        assume

         A6: x in (N + {w});

        then

        reconsider x as Element of V;

        x in { (u + v) where u,v be Element of V : u in N & v in {w} } by A6, RUSUB_4:def 9;

        then

        consider u2,v2 be Element of V such that

         A7: x = (u2 + v2) and

         A8: u2 in N and

         A9: v2 in {w};

        x = (u2 + (u1 + v1)) by A7, A9, TARSKI:def 1

        .= ((u2 + u1) + v1) by RLVECT_1:def 3;

        

        then (x - v1) = ((u2 + u1) + (v1 - v1)) by RLVECT_1:def 3

        .= ((u2 + u1) + ( 0. V)) by RLVECT_1: 15

        .= (u2 + u1);

        then (x - v1) in { (u + v) where u,v be Element of V : u in N & v in {u1} } by A8, A5;

        then

         A10: (x - v1) in L by A4, RUSUB_4:def 9;

        set y = (x - v1);

        

         A11: v1 in {v1} by TARSKI:def 1;

        (y + v1) = (x - (v1 - v1)) by RLVECT_1: 29

        .= (x - ( 0. V)) by RLVECT_1: 15

        .= x;

        then x in { (u + v) where u,v be Element of V : u in L & v in {v1} } by A10, A11;

        hence thesis by A3, RUSUB_4:def 9;

      end;

      then

       A12: (N + {w}) c= M;

      for x be object st x in M holds x in (N + {w})

      proof

        let x be object;

        

         A13: w in {w} by TARSKI:def 1;

        assume

         A14: x in M;

        then

        reconsider x as Element of V;

        x in { (u + v) where u,v be Element of V : u in L & v in {v1} } by A3, A14, RUSUB_4:def 9;

        then

        consider u2,v2 be Element of V such that

         A15: x = (u2 + v2) and

         A16: u2 in L and

         A17: v2 in {v1};

        

         A18: v2 = v1 by A17, TARSKI:def 1;

        u2 in { (u + v) where u,v be Element of V : u in N & v in {u1} } by A4, A16, RUSUB_4:def 9;

        then

        consider u3,v3 be Element of V such that

         A19: u2 = (u3 + v3) and

         A20: u3 in N and

         A21: v3 in {u1};

        v3 = u1 by A21, TARSKI:def 1;

        then x = (u3 + w) by A15, A19, A18, RLVECT_1:def 3;

        then x in { (u + v) where u,v be Element of V : u in N & v in {w} } by A20, A13;

        hence thesis by RUSUB_4:def 9;

      end;

      then M c= (N + {w});

      then M = (N + {w}) by A12;

      hence thesis;

    end;

    definition

      let V be non empty addLoopStr, M,N be Subset of V;

      :: RUSUB_5:def2

      func M - N -> Subset of V equals { (u - v) where u,v be Element of V : u in M & v in N };

      coherence

      proof

        defpred P[ set, set] means $1 in M & $2 in N;

        deffunc F( Element of V, Element of V) = ($1 - $2);

        { F(u,v) where u,v be Element of V : P[u, v] } is Subset of V from DOMAIN_1:sch 9;

        hence thesis;

      end;

    end

    theorem :: RUSUB_5:4

    

     Th4: for V be RealLinearSpace, M,N be Affine Subset of V holds (M - N) is Affine

    proof

      let V be RealLinearSpace;

      let M,N be Affine Subset of V;

      for x,y be VECTOR of V, a be Real st x in (M - N) & y in (M - N) holds (((1 - a) * x) + (a * y)) in (M - N)

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume that

         A1: x in (M - N) and

         A2: y in (M - N);

        consider u1,v1 be Element of V such that

         A3: x = (u1 - v1) and

         A4: u1 in M & v1 in N by A1;

        consider u2,v2 be Element of V such that

         A5: y = (u2 - v2) and

         A6: u2 in M & v2 in N by A2;

        

         A7: (((1 - a) * x) + (a * y)) = ((((1 - a) * u1) - ((1 - a) * v1)) + (a * (u2 - v2))) by A3, A5, RLVECT_1: 34

        .= ((((1 - a) * u1) - ((1 - a) * v1)) + ((a * u2) - (a * v2))) by RLVECT_1: 34

        .= (((((1 - a) * u1) + ( - ((1 - a) * v1))) + (a * u2)) - (a * v2)) by RLVECT_1:def 3

        .= (((((1 - a) * u1) + (a * u2)) + ( - ((1 - a) * v1))) + ( - (a * v2))) by RLVECT_1:def 3

        .= ((((1 - a) * u1) + (a * u2)) + (( - ((1 - a) * v1)) + ( - (a * v2)))) by RLVECT_1:def 3

        .= ((((1 - a) * u1) + (a * u2)) - (((1 - a) * v1) + (a * v2))) by RLVECT_1: 31;

        (((1 - a) * u1) + (a * u2)) in M & (((1 - a) * v1) + (a * v2)) in N by A4, A6, RUSUB_4:def 4;

        hence thesis by A7;

      end;

      hence thesis by RUSUB_4:def 4;

    end;

    theorem :: RUSUB_5:5

    for V be non empty addLoopStr, M,N be Subset of V st M is empty or N is empty holds (M + N) is empty

    proof

      let V be non empty addLoopStr;

      let M,N be Subset of V;

      assume

       A1: M is empty or N is empty;

      assume not (M + N) is empty;

      then

      consider x be object such that

       A2: x in (M + N);

      x in { (u + v) where u,v be Element of V : u in M & v in N } by A2, RUSUB_4:def 9;

      then ex u,v be Element of V st x = (u + v) & u in M & v in N;

      hence contradiction by A1;

    end;

    theorem :: RUSUB_5:6

    for V be non empty addLoopStr, M,N be non empty Subset of V holds (M + N) is non empty

    proof

      let V be non empty addLoopStr;

      let M,N be non empty Subset of V;

      consider x be object such that

       A1: x in M by XBOOLE_0:def 1;

      consider y be object such that

       A2: y in N by XBOOLE_0:def 1;

      reconsider x, y as Element of V by A1, A2;

      (x + y) in { (u + v) where u,v be Element of V : u in M & v in N } by A1, A2;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RUSUB_5:7

    for V be non empty addLoopStr, M,N be Subset of V st M is empty or N is empty holds (M - N) is empty

    proof

      let V be non empty addLoopStr;

      let M,N be Subset of V;

      assume

       A1: M is empty or N is empty;

      assume not (M - N) is empty;

      then

      consider x be object such that

       A2: x in (M - N);

      ex u,v be Element of V st x = (u - v) & u in M & v in N by A2;

      hence contradiction by A1;

    end;

    theorem :: RUSUB_5:8

    

     Th8: for V be non empty addLoopStr, M,N be non empty Subset of V holds (M - N) is non empty

    proof

      let V be non empty addLoopStr;

      let M,N be non empty Subset of V;

      consider x be object such that

       A1: x in M by XBOOLE_0:def 1;

      consider y be object such that

       A2: y in N by XBOOLE_0:def 1;

      reconsider x, y as Element of V by A1, A2;

      (x - y) in { (u - v) where u,v be Element of V : u in M & v in N } by A1, A2;

      hence thesis;

    end;

    theorem :: RUSUB_5:9

    

     Th9: for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, M,N be Subset of V, v be Element of V holds M = (N + {v}) iff (M - {v}) = N

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let M,N be Subset of V;

      let v be Element of V;

      

       A1: (M - {v}) = N implies M = (N + {v})

      proof

        assume

         A2: (M - {v}) = N;

        for x be object st x in (N + {v}) holds x in M

        proof

          let x be object;

          assume

           A3: x in (N + {v});

          then

          reconsider x as Element of V;

          x in { (u1 + v1) where u1,v1 be Element of V : u1 in N & v1 in {v} } by A3, RUSUB_4:def 9;

          then

          consider u1,v1 be Element of V such that

           A4: x = (u1 + v1) and

           A5: u1 in N and

           A6: v1 in {v};

          

           A7: (x - v1) = (u1 + (v1 - v1)) by A4, RLVECT_1:def 3

          .= (u1 + ( 0. V)) by RLVECT_1: 15

          .= u1;

          v1 = v by A6, TARSKI:def 1;

          then

          consider u2,v2 be Element of V such that

           A8: (x - v) = (u2 - v2) and

           A9: u2 in M and

           A10: v2 in {v} by A2, A5, A7;

          v2 = v by A10, TARSKI:def 1;

          

          then ((x - v) + v) = (u2 - (v - v)) by A8, RLVECT_1: 29

          .= (u2 - ( 0. V)) by RLVECT_1: 15

          .= u2;

          

          then u2 = (x - (v - v)) by RLVECT_1: 29

          .= (x - ( 0. V)) by RLVECT_1: 15;

          hence thesis by A9;

        end;

        then

         A11: (N + {v}) c= M;

        for x be object st x in M holds x in (N + {v})

        proof

          let x be object;

          assume

           A12: x in M;

          then

          reconsider x as Element of V;

          

           A13: v in {v} by TARSKI:def 1;

          then (x - v) in { (u2 - v2) where u2,v2 be Element of V : u2 in M & v2 in {v} } by A12;

          then

          consider u2 be Element of V such that

           A14: (x - v) = u2 and

           A15: u2 in N by A2;

          (u2 + v) = (x - (v - v)) by A14, RLVECT_1: 29

          .= (x - ( 0. V)) by RLVECT_1: 15

          .= x;

          then x in { (u1 + v1) where u1,v1 be Element of V : u1 in N & v1 in {v} } by A13, A15;

          hence thesis by RUSUB_4:def 9;

        end;

        then M c= (N + {v});

        hence thesis by A11;

      end;

      M = (N + {v}) implies (M - {v}) = N

      proof

        assume

         A16: M = (N + {v});

        for x be object st x in (M - {v}) holds x in N

        proof

          let x be object;

          assume

           A17: x in (M - {v});

          then

          reconsider x as Element of V;

          consider u1,v1 be Element of V such that

           A18: x = (u1 - v1) and

           A19: u1 in M and

           A20: v1 in {v} by A17;

          

           A21: (x + v1) = (u1 - (v1 - v1)) by A18, RLVECT_1: 29

          .= (u1 - ( 0. V)) by RLVECT_1: 15

          .= u1;

          v1 = v by A20, TARSKI:def 1;

          then (x + v) in { (u2 + v2) where u2,v2 be Element of V : u2 in N & v2 in {v} } by A16, A19, A21, RUSUB_4:def 9;

          then

          consider u2,v2 be Element of V such that

           A22: (x + v) = (u2 + v2) & u2 in N and

           A23: v2 in {v};

          v2 = v by A23, TARSKI:def 1;

          hence thesis by A22, RLVECT_1: 8;

        end;

        then

         A24: (M - {v}) c= N;

        for x be object st x in N holds x in (M - {v})

        proof

          let x be object;

          assume

           A25: x in N;

          then

          reconsider x as Element of V;

          

           A26: v in {v} by TARSKI:def 1;

          then (x + v) in { (u2 + v2) where u2,v2 be Element of V : u2 in N & v2 in {v} } by A25;

          then (x + v) in M by A16, RUSUB_4:def 9;

          then

          consider u2 be Element of V such that

           A27: (x + v) = u2 and

           A28: u2 in M;

          (u2 - v) = (x + (v - v)) by A27, RLVECT_1:def 3

          .= (x + ( 0. V)) by RLVECT_1: 15

          .= x;

          hence thesis by A26, A28;

        end;

        then N c= (M - {v});

        hence thesis by A24;

      end;

      hence thesis by A1;

    end;

    theorem :: RUSUB_5:10

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, M,N be Subset of V, v be Element of V st v in N holds (M + {v}) c= (M + N)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let M,N be Subset of V;

      let v be Element of V;

      assume

       A1: v in N;

      let x be object;

      assume

       A2: x in (M + {v});

      then

      reconsider x as Element of V;

      x in { (u1 + v1) where u1,v1 be Element of V : u1 in M & v1 in {v} } by A2, RUSUB_4:def 9;

      then

      consider u2,v2 be Element of V such that

       A3: x = (u2 + v2) and

       A4: u2 in M and

       A5: v2 in {v};

      x = (u2 + v) by A3, A5, TARSKI:def 1;

      then x in { (u1 + v1) where u1,v1 be Element of V : u1 in M & v1 in N } by A1, A4;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RUSUB_5:11

    for V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr, M,N be Subset of V, v be Element of V st v in N holds (M - {v}) c= (M - N)

    proof

      let V be Abelian add-associative right_zeroed right_complementable non empty addLoopStr;

      let M,N be Subset of V;

      let v be Element of V;

      assume

       A1: v in N;

      let x be object;

      assume

       A2: x in (M - {v});

      then

      reconsider x as Element of V;

      consider u2,v2 be Element of V such that

       A3: x = (u2 - v2) and

       A4: u2 in M and

       A5: v2 in {v} by A2;

      x = (u2 - v) by A3, A5, TARSKI:def 1;

      hence thesis by A1, A4;

    end;

    theorem :: RUSUB_5:12

    

     Th12: for V be RealLinearSpace, M be non empty Subset of V holds ( 0. V) in (M - M)

    proof

      let V be RealLinearSpace;

      let M be non empty Subset of V;

      consider v be object such that

       A1: v in M by XBOOLE_0:def 1;

      reconsider v as Element of V by A1;

      (v - v) in { (u1 - v1) where u1,v1 be Element of V : u1 in M & v1 in M } by A1;

      hence thesis by RLVECT_1: 15;

    end;

    theorem :: RUSUB_5:13

    

     Th13: for V be RealLinearSpace, M be non empty Affine Subset of V, v be VECTOR of V st M is Subspace-like & v in M holds (M + {v}) c= M

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      let v be VECTOR of V;

      assume

       A1: M is Subspace-like & v in M;

      let x be object;

      assume

       A2: x in (M + {v});

      then

      reconsider x as Element of V;

      x in { (u1 + v1) where u1,v1 be Element of V : u1 in M & v1 in {v} } by A2, RUSUB_4:def 9;

      then

      consider u1,v1 be Element of V such that

       A3: x = (u1 + v1) & u1 in M and

       A4: v1 in {v};

      v1 = v by A4, TARSKI:def 1;

      hence thesis by A1, A3, RUSUB_4:def 7;

    end;

    theorem :: RUSUB_5:14

    

     Th14: for V be RealLinearSpace, M be non empty Affine Subset of V, N1,N2 be non empty Affine Subset of V st N1 is Subspace-like & N2 is Subspace-like & M is_parallel_to N1 & M is_parallel_to N2 holds N1 = N2

    proof

      let V be RealLinearSpace;

      let M,N1,N2 be non empty Affine Subset of V;

      assume that

       A1: N1 is Subspace-like and

       A2: N2 is Subspace-like and

       A3: M is_parallel_to N1 and

       A4: M is_parallel_to N2;

      N2 is_parallel_to M by A4, Th2;

      then N2 is_parallel_to N1 by A3, Th3;

      then

      consider v2 be VECTOR of V such that

       A5: N2 = (N1 + {v2});

      N1 is_parallel_to M by A3, Th2;

      then N1 is_parallel_to N2 by A4, Th3;

      then

      consider v1 be VECTOR of V such that

       A6: N1 = (N2 + {v1});

      ( 0. V) in N2 by A2, RUSUB_4:def 7;

      then ( 0. V) in { (p + q) where p,q be Element of V : p in N1 & q in {v2} } by A5, RUSUB_4:def 9;

      then

      consider p2,q2 be Element of V such that

       A7: ( 0. V) = (p2 + q2) and

       A8: p2 in N1 and

       A9: q2 in {v2};

      ( 0. V) = (p2 + v2) by A7, A9, TARSKI:def 1;

      then

       A10: ( - v2) in N1 by A8, RLVECT_1: 6;

      v2 = ( - ( - v2))

      .= (( - 1) * ( - v2)) by RLVECT_1: 16;

      then v2 in N1 by A1, A10, RUSUB_4:def 7;

      then

       A11: N2 c= N1 by A1, A5, Th13;

      ( 0. V) in N1 by A1, RUSUB_4:def 7;

      then ( 0. V) in { (p + q) where p,q be Element of V : p in N2 & q in {v1} } by A6, RUSUB_4:def 9;

      then

      consider p1,q1 be Element of V such that

       A12: ( 0. V) = (p1 + q1) and

       A13: p1 in N2 and

       A14: q1 in {v1};

      ( 0. V) = (p1 + v1) by A12, A14, TARSKI:def 1;

      then

       A15: ( - v1) in N2 by A13, RLVECT_1: 6;

      v1 = ( - ( - v1))

      .= (( - 1) * ( - v1)) by RLVECT_1: 16;

      then v1 in N2 by A2, A15, RUSUB_4:def 7;

      then N1 c= N2 by A2, A6, Th13;

      hence thesis by A11;

    end;

    theorem :: RUSUB_5:15

    

     Th15: for V be RealLinearSpace, M be non empty Affine Subset of V, v be VECTOR of V st v in M holds ( 0. V) in (M - {v})

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      let v be VECTOR of V;

      

       A1: v in {v} & ( 0. V) = (v - v) by RLVECT_1: 15, TARSKI:def 1;

      assume v in M;

      hence thesis by A1;

    end;

    theorem :: RUSUB_5:16

    

     Th16: for V be RealLinearSpace, M be non empty Affine Subset of V, v be VECTOR of V st v in M holds ex N be non empty Affine Subset of V st N = (M - {v}) & M is_parallel_to N & N is Subspace-like

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      let v be VECTOR of V;

       {v} is non empty Affine by RUSUB_4: 23;

      then

      reconsider N = (M - {v}) as non empty Affine Subset of V by Th4, Th8;

      assume v in M;

      then

       A1: ( 0. V) in N by Th15;

      take N;

      M is_parallel_to N

      proof

        take v;

        thus thesis by Th9;

      end;

      hence thesis by A1, RUSUB_4: 26;

    end;

    theorem :: RUSUB_5:17

    

     Th17: for V be RealLinearSpace, M be non empty Affine Subset of V, u,v be VECTOR of V st u in M & v in M holds (M - {v}) = (M - {u})

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      let u,v be VECTOR of V;

      assume u in M & v in M;

      then (ex N1 be non empty Affine Subset of V st N1 = (M - {u}) & M is_parallel_to N1 & N1 is Subspace-like) & ex N2 be non empty Affine Subset of V st N2 = (M - {v}) & M is_parallel_to N2 & N2 is Subspace-like by Th16;

      hence thesis by Th14;

    end;

    theorem :: RUSUB_5:18

    

     Th18: for V be RealLinearSpace, M be non empty Affine Subset of V holds (M - M) = ( union { (M - {v}) where v be VECTOR of V : v in M })

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      for x be object st x in (M - M) holds x in ( union { (M - {v}) where v be VECTOR of V : v in M })

      proof

        let x be object;

        assume

         A1: x in (M - M);

        then

        reconsider x as Element of V;

        consider u1,v1 be Element of V such that

         A2: x = (u1 - v1) & u1 in M and

         A3: v1 in M by A1;

        v1 in {v1} by TARSKI:def 1;

        then

         A4: x in { (p - q) where p,q be Element of V : p in M & q in {v1} } by A2;

        (M - {v1}) in { (M - {v}) where v be VECTOR of V : v in M } by A3;

        hence thesis by A4, TARSKI:def 4;

      end;

      then

       A5: (M - M) c= ( union { (M - {v}) where v be VECTOR of V : v in M });

      for x be object st x in ( union { (M - {v}) where v be VECTOR of V : v in M }) holds x in (M - M)

      proof

        let x be object;

        assume x in ( union { (M - {v}) where v be VECTOR of V : v in M });

        then

        consider N be set such that

         A6: x in N and

         A7: N in { (M - {v}) where v be VECTOR of V : v in M } by TARSKI:def 4;

        consider v1 be VECTOR of V such that

         A8: N = (M - {v1}) and

         A9: v1 in M by A7;

        consider p1,q1 be Element of V such that

         A10: x = (p1 - q1) & p1 in M and

         A11: q1 in {v1} by A6, A8;

        q1 = v1 by A11, TARSKI:def 1;

        hence thesis by A9, A10;

      end;

      then ( union { (M - {v}) where v be VECTOR of V : v in M }) c= (M - M);

      hence thesis by A5;

    end;

    theorem :: RUSUB_5:19

    

     Th19: for V be RealLinearSpace, M be non empty Affine Subset of V, v be VECTOR of V st v in M holds (M - {v}) = ( union { (M - {u}) where u be VECTOR of V : u in M })

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      let v be VECTOR of V;

      assume

       A1: v in M;

      for x be object st x in ( union { (M - {u}) where u be VECTOR of V : u in M }) holds x in (M - {v})

      proof

        let x be object;

        assume x in ( union { (M - {u}) where u be VECTOR of V : u in M });

        then

        consider N be set such that

         A2: x in N and

         A3: N in { (M - {u}) where u be VECTOR of V : u in M } by TARSKI:def 4;

        ex v1 be VECTOR of V st N = (M - {v1}) & v1 in M by A3;

        hence thesis by A1, A2, Th17;

      end;

      then

       A4: ( union { (M - {u}) where u be VECTOR of V : u in M }) c= (M - {v});

      for x be object st x in (M - {v}) holds x in ( union { (M - {u}) where u be VECTOR of V : u in M })

      proof

        let x be object;

        assume

         A5: x in (M - {v});

        (M - {v}) in { (M - {u}) where u be VECTOR of V : u in M } by A1;

        hence thesis by A5, TARSKI:def 4;

      end;

      then (M - {v}) c= ( union { (M - {u}) where u be VECTOR of V : u in M });

      hence thesis by A4;

    end;

    theorem :: RUSUB_5:20

    for V be RealLinearSpace, M be non empty Affine Subset of V holds ex L be non empty Affine Subset of V st L = (M - M) & L is Subspace-like & M is_parallel_to L

    proof

      let V be RealLinearSpace;

      let M be non empty Affine Subset of V;

      reconsider L = (M - M) as non empty Affine Subset of V by Th4, Th8;

      consider v be object such that

       A1: v in M by XBOOLE_0:def 1;

      reconsider v as VECTOR of V by A1;

      take L;

      

       A2: ( 0. V) in L by Th12;

       {v} is non empty Affine by RUSUB_4: 23;

      then

      reconsider N = (M - {v}) as non empty Affine Subset of V by Th4, Th8;

      

       A3: M is_parallel_to N

      proof

        take v;

        thus thesis by Th9;

      end;

      N = ( union { (M - {u}) where u be VECTOR of V : u in M }) by A1, Th19

      .= L by Th18;

      hence thesis by A3, A2, RUSUB_4: 26;

    end;

    begin

    definition

      let V be RealUnitarySpace, W be Subspace of V;

      :: RUSUB_5:def3

      func Ort_Comp W -> strict Subspace of V means

      : Def3: the carrier of it = { v where v be VECTOR of V : for w be VECTOR of V st w in W holds (w,v) are_orthogonal };

      existence

      proof

        defpred P[ VECTOR of V] means for w be VECTOR of V st w in W holds (w,$1) are_orthogonal ;

        reconsider A = { v where v be VECTOR of V : P[v] } as Subset of V from DOMAIN_1:sch 7;

        

         A1: for v,u be VECTOR of V st v in A & u in A holds (v + u) in A

        proof

          let v,u be VECTOR of V;

          assume that

           A2: v in A and

           A3: u in A;

          for w be VECTOR of V st w in W holds (w,(v + u)) are_orthogonal

          proof

            let w be VECTOR of V;

            assume

             A4: w in W;

            ex u9 be VECTOR of V st u = u9 & for w be VECTOR of V st w in W holds (w,u9) are_orthogonal by A3;

            then (w,u) are_orthogonal by A4;

            then

             A5: (w .|. u) = 0 by BHSP_1:def 3;

            ex v9 be VECTOR of V st v = v9 & for w be VECTOR of V st w in W holds (w,v9) are_orthogonal by A2;

            then (w,v) are_orthogonal by A4;

            then (w .|. v) = 0 by BHSP_1:def 3;

            then (w .|. (v + u)) = ( 0 + 0 ) by A5, BHSP_1: 2;

            hence thesis by BHSP_1:def 3;

          end;

          hence thesis;

        end;

        for w be VECTOR of V st w in W holds (w,( 0. V)) are_orthogonal

        proof

          let w be VECTOR of V;

          assume w in W;

          (w .|. ( 0. V)) = 0 by BHSP_1: 15;

          hence thesis by BHSP_1:def 3;

        end;

        then

         A6: ( 0. V) in A;

        for a be Real, v be VECTOR of V st v in A holds (a * v) in A

        proof

          let a be Real;

          let v be VECTOR of V;

          assume v in A;

          then

           A7: ex v9 be VECTOR of V st v = v9 & for w be VECTOR of V st w in W holds (w,v9) are_orthogonal ;

          for w be VECTOR of V st w in W holds (w,(a * v)) are_orthogonal

          proof

            let w be VECTOR of V;

            assume w in W;

            then

             A8: (w,v) are_orthogonal by A7;

            (w .|. (a * v)) = (a * (w .|. v)) by BHSP_1: 3

            .= (a * 0 ) by A8, BHSP_1:def 3;

            hence thesis by BHSP_1:def 3;

          end;

          hence thesis;

        end;

        then A is linearly-closed by A1, RLSUB_1:def 1;

        hence thesis by A6, RUSUB_1: 29;

      end;

      uniqueness by RUSUB_1: 24;

    end

    definition

      let V be RealUnitarySpace, M be non empty Subset of V;

      :: RUSUB_5:def4

      func Ort_Comp M -> strict Subspace of V means

      : Def4: the carrier of it = { v where v be VECTOR of V : for w be VECTOR of V st w in M holds (w,v) are_orthogonal };

      existence

      proof

        defpred P[ VECTOR of V] means for w be VECTOR of V st w in M holds (w,$1) are_orthogonal ;

        reconsider A = { v where v be VECTOR of V : P[v] } as Subset of V from DOMAIN_1:sch 7;

        

         A1: for v,u be VECTOR of V st v in A & u in A holds (v + u) in A

        proof

          let v,u be VECTOR of V;

          assume that

           A2: v in A and

           A3: u in A;

          for w be VECTOR of V st w in M holds (w,(v + u)) are_orthogonal

          proof

            let w be VECTOR of V;

            assume

             A4: w in M;

            ex u9 be VECTOR of V st u = u9 & for w be VECTOR of V st w in M holds (w,u9) are_orthogonal by A3;

            then (w,u) are_orthogonal by A4;

            then

             A5: (w .|. u) = 0 by BHSP_1:def 3;

            ex v9 be VECTOR of V st v = v9 & for w be VECTOR of V st w in M holds (w,v9) are_orthogonal by A2;

            then (w,v) are_orthogonal by A4;

            then (w .|. v) = 0 by BHSP_1:def 3;

            then (w .|. (v + u)) = ( 0 + 0 ) by A5, BHSP_1: 2;

            hence thesis by BHSP_1:def 3;

          end;

          hence thesis;

        end;

        for w be VECTOR of V st w in M holds (w,( 0. V)) are_orthogonal

        proof

          let w be VECTOR of V;

          assume w in M;

          (w .|. ( 0. V)) = 0 by BHSP_1: 15;

          hence thesis by BHSP_1:def 3;

        end;

        then

         A6: ( 0. V) in A;

        for a be Real, v be VECTOR of V st v in A holds (a * v) in A

        proof

          let a be Real;

          let v be VECTOR of V;

          assume v in A;

          then

           A7: ex v9 be VECTOR of V st v = v9 & for w be VECTOR of V st w in M holds (w,v9) are_orthogonal ;

          for w be VECTOR of V st w in M holds (w,(a * v)) are_orthogonal

          proof

            let w be VECTOR of V;

            assume w in M;

            then

             A8: (w,v) are_orthogonal by A7;

            (w .|. (a * v)) = (a * (w .|. v)) by BHSP_1: 3

            .= (a * 0 ) by A8, BHSP_1:def 3;

            hence thesis by BHSP_1:def 3;

          end;

          hence thesis;

        end;

        then A is linearly-closed by A1, RLSUB_1:def 1;

        hence thesis by A6, RUSUB_1: 29;

      end;

      uniqueness by RUSUB_1: 24;

    end

    theorem :: RUSUB_5:21

    for V be RealUnitarySpace, W be Subspace of V holds ( 0. V) in ( Ort_Comp W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      for w be VECTOR of V st w in W holds (w,( 0. V)) are_orthogonal

      proof

        let w be VECTOR of V;

        assume w in W;

        (w .|. ( 0. V)) = 0 by BHSP_1: 15;

        hence thesis by BHSP_1:def 3;

      end;

      then ( 0. V) in { v where v be VECTOR of V : for w be VECTOR of V st w in W holds (w,v) are_orthogonal };

      then ( 0. V) in the carrier of ( Ort_Comp W) by Def3;

      hence thesis;

    end;

    theorem :: RUSUB_5:22

    for V be RealUnitarySpace holds ( Ort_Comp ( (0). V)) = ( (Omega). V)

    proof

      let V be RealUnitarySpace;

      for x be object st x in the carrier of ( (Omega). V) holds x in the carrier of ( Ort_Comp ( (0). V))

      proof

        let x be object;

        assume x in the carrier of ( (Omega). V);

        then x in ( (Omega). V);

        then x in the UNITSTR of V by RUSUB_1:def 3;

        then

        reconsider x as Element of V;

        for w be VECTOR of V st w in ( (0). V) holds (w,x) are_orthogonal

        proof

          let w be VECTOR of V;

          assume w in ( (0). V);

          then w in the carrier of ( (0). V);

          then w in {( 0. V)} by RUSUB_1:def 2;

          

          then (w .|. x) = (( 0. V) .|. x) by TARSKI:def 1

          .= 0 by BHSP_1: 14;

          hence thesis by BHSP_1:def 3;

        end;

        then x in { v where v be VECTOR of V : for w be VECTOR of V st w in ( (0). V) holds (w,v) are_orthogonal };

        hence thesis by Def3;

      end;

      then

       A1: the carrier of ( (Omega). V) c= the carrier of ( Ort_Comp ( (0). V));

      for x be object st x in the carrier of ( Ort_Comp ( (0). V)) holds x in the carrier of ( (Omega). V)

      proof

        let x be object;

        assume x in the carrier of ( Ort_Comp ( (0). V));

        then x in ( Ort_Comp ( (0). V));

        then x in V by RUSUB_1: 2;

        then x in the carrier of V;

        then x in the UNITSTR of V;

        then x in ( (Omega). V) by RUSUB_1:def 3;

        hence thesis;

      end;

      then the carrier of ( Ort_Comp ( (0). V)) c= the carrier of ( (Omega). V);

      then the carrier of ( (Omega). V) = the carrier of ( Ort_Comp ( (0). V)) by A1;

      hence thesis by RUSUB_1: 24;

    end;

    theorem :: RUSUB_5:23

    for V be RealUnitarySpace holds ( Ort_Comp ( (Omega). V)) = ( (0). V)

    proof

      let V be RealUnitarySpace;

      for x be object st x in the carrier of ( Ort_Comp ( (Omega). V)) holds x in the carrier of ( (0). V)

      proof

        let x be object;

        assume x in the carrier of ( Ort_Comp ( (Omega). V));

        then x in { v where v be VECTOR of V : for w be VECTOR of V st w in ( (Omega). V) holds (w,v) are_orthogonal } by Def3;

        then

         A1: ex v be VECTOR of V st x = v & for w be VECTOR of V st w in ( (Omega). V) holds (w,v) are_orthogonal ;

        then

        reconsider x as VECTOR of V;

        x in the UNITSTR of V;

        then x in ( (Omega). V) by RUSUB_1:def 3;

        then (x,x) are_orthogonal by A1;

        then 0 = (x .|. x) by BHSP_1:def 3;

        then x = ( 0. V) by BHSP_1:def 2;

        then x in {( 0. V)} by TARSKI:def 1;

        hence thesis by RUSUB_1:def 2;

      end;

      then

       A2: the carrier of ( Ort_Comp ( (Omega). V)) c= the carrier of ( (0). V);

      for x be object st x in the carrier of ( (0). V) holds x in the carrier of ( Ort_Comp ( (Omega). V))

      proof

        let x be object;

        assume x in the carrier of ( (0). V);

        then

         A3: x in {( 0. V)} by RUSUB_1:def 2;

        then

        reconsider x as VECTOR of V;

        for w be VECTOR of V st w in ( (Omega). V) holds (w,x) are_orthogonal

        proof

          let w be VECTOR of V;

          assume w in ( (Omega). V);

          (w .|. x) = (w .|. ( 0. V)) by A3, TARSKI:def 1

          .= 0 by BHSP_1: 15;

          hence thesis by BHSP_1:def 3;

        end;

        then x in { v where v be VECTOR of V : for w be VECTOR of V st w in ( (Omega). V) holds (w,v) are_orthogonal };

        hence thesis by Def3;

      end;

      then the carrier of ( (0). V) c= the carrier of ( Ort_Comp ( (Omega). V));

      then the carrier of ( Ort_Comp ( (Omega). V)) = the carrier of ( (0). V) by A2;

      hence thesis by RUSUB_1: 24;

    end;

    theorem :: RUSUB_5:24

    for V be RealUnitarySpace, W be Subspace of V, v be VECTOR of V st v <> ( 0. V) holds v in W implies not v in ( Ort_Comp W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let v be VECTOR of V;

      assume

       A1: v <> ( 0. V);

      v in W implies not v in ( Ort_Comp W)

      proof

        assume

         A2: v in W;

        assume v in ( Ort_Comp W);

        then v in the carrier of ( Ort_Comp W);

        then v in { v1 where v1 be VECTOR of V : for w be VECTOR of V st w in W holds (w,v1) are_orthogonal } by Def3;

        then ex v1 be VECTOR of V st v = v1 & for w be VECTOR of V st w in W holds (w,v1) are_orthogonal ;

        then (v,v) are_orthogonal by A2;

        then 0 = (v .|. v) by BHSP_1:def 3;

        hence contradiction by A1, BHSP_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_5:25

    

     Th25: for V be RealUnitarySpace, M be non empty Subset of V holds M c= the carrier of ( Ort_Comp ( Ort_Comp M))

    proof

      let V be RealUnitarySpace;

      let M be non empty Subset of V;

      let x be object;

      assume

       A1: x in M;

      then

      reconsider x as VECTOR of V;

      for y be VECTOR of V st y in ( Ort_Comp M) holds (x,y) are_orthogonal

      proof

        let y be VECTOR of V;

        assume y in ( Ort_Comp M);

        then y in the carrier of ( Ort_Comp M);

        then y in { v where v be VECTOR of V : for w be VECTOR of V st w in M holds (w,v) are_orthogonal } by Def4;

        then ex v be VECTOR of V st y = v & for w be VECTOR of V st w in M holds (w,v) are_orthogonal ;

        hence thesis by A1;

      end;

      then x in { v where v be VECTOR of V : for w be VECTOR of V st w in ( Ort_Comp M) holds (w,v) are_orthogonal };

      hence thesis by Def3;

    end;

    theorem :: RUSUB_5:26

    

     Th26: for V be RealUnitarySpace, M,N be non empty Subset of V st M c= N holds the carrier of ( Ort_Comp N) c= the carrier of ( Ort_Comp M)

    proof

      let V be RealUnitarySpace;

      let M,N be non empty Subset of V;

      assume

       A1: M c= N;

      let x be object;

      assume x in the carrier of ( Ort_Comp N);

      then x in { v where v be VECTOR of V : for w be VECTOR of V st w in N holds (w,v) are_orthogonal } by Def4;

      then

       A2: ex v1 be VECTOR of V st x = v1 & for w be VECTOR of V st w in N holds (w,v1) are_orthogonal ;

      then

      reconsider x as VECTOR of V;

      for y be VECTOR of V st y in M holds (y,x) are_orthogonal by A1, A2;

      then x in { v where v be VECTOR of V : for w be VECTOR of V st w in M holds (w,v) are_orthogonal };

      hence thesis by Def4;

    end;

    theorem :: RUSUB_5:27

    

     Th27: for V be RealUnitarySpace, W be Subspace of V, M be non empty Subset of V st M = the carrier of W holds ( Ort_Comp M) = ( Ort_Comp W)

    proof

      let V be RealUnitarySpace;

      let W be Subspace of V;

      let M be non empty Subset of V;

      assume

       A1: M = the carrier of W;

      for x be object st x in the carrier of ( Ort_Comp W) holds x in the carrier of ( Ort_Comp M)

      proof

        let x be object;

        assume x in the carrier of ( Ort_Comp W);

        then x in { v where v be VECTOR of V : for w be VECTOR of V st w in W holds (w,v) are_orthogonal } by Def3;

        then

        consider v be VECTOR of V such that

         A2: x = v and

         A3: for w be VECTOR of V st w in W holds (w,v) are_orthogonal ;

        for w be VECTOR of V st w in M holds (w,v) are_orthogonal by A1, STRUCT_0:def 5, A3;

        then x in { v1 where v1 be VECTOR of V : for w be VECTOR of V st w in M holds (w,v1) are_orthogonal } by A2;

        hence thesis by Def4;

      end;

      then

       A4: the carrier of ( Ort_Comp W) c= the carrier of ( Ort_Comp M);

      for x be object st x in the carrier of ( Ort_Comp M) holds x in the carrier of ( Ort_Comp W)

      proof

        let x be object;

        assume x in the carrier of ( Ort_Comp M);

        then x in { v where v be VECTOR of V : for w be VECTOR of V st w in M holds (w,v) are_orthogonal } by Def4;

        then

        consider v be VECTOR of V such that

         A5: x = v and

         A6: for w be VECTOR of V st w in M holds (w,v) are_orthogonal ;

        for w be VECTOR of V st w in W holds (w,v) are_orthogonal by A1, A6;

        then x in { v1 where v1 be VECTOR of V : for w be VECTOR of V st w in W holds (w,v1) are_orthogonal } by A5;

        hence thesis by Def3;

      end;

      then the carrier of ( Ort_Comp M) c= the carrier of ( Ort_Comp W);

      then the carrier of ( Ort_Comp W) = the carrier of ( Ort_Comp M) by A4;

      hence thesis by RUSUB_1: 24;

    end;

    theorem :: RUSUB_5:28

    for V be RealUnitarySpace, M be non empty Subset of V holds ( Ort_Comp M) = ( Ort_Comp ( Ort_Comp ( Ort_Comp M)))

    proof

      let V be RealUnitarySpace;

      let M be non empty Subset of V;

      set N = the carrier of ( Ort_Comp M);

      reconsider N as Subset of V by RUSUB_1:def 1;

      reconsider N as non empty Subset of V;

      set L = the carrier of ( Ort_Comp ( Ort_Comp M));

      reconsider L as Subset of V by RUSUB_1:def 1;

      reconsider L as non empty Subset of V;

      N c= the carrier of ( Ort_Comp ( Ort_Comp N)) by Th25;

      then

       A1: N c= the carrier of ( Ort_Comp ( Ort_Comp ( Ort_Comp M))) by Th27;

      the carrier of ( Ort_Comp L) c= the carrier of ( Ort_Comp M) by Th25, Th26;

      then the carrier of ( Ort_Comp ( Ort_Comp ( Ort_Comp M))) c= the carrier of ( Ort_Comp M) by Th27;

      then the carrier of ( Ort_Comp ( Ort_Comp ( Ort_Comp M))) = the carrier of ( Ort_Comp M) by A1;

      hence thesis by RUSUB_1: 24;

    end;

    theorem :: RUSUB_5:29

    

     Th29: for V be RealUnitarySpace, x,y be VECTOR of V holds ( ||.(x + y).|| ^2 ) = ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) & ( ||.(x - y).|| ^2 ) = ((( ||.x.|| ^2 ) - (2 * (x .|. y))) + ( ||.y.|| ^2 ))

    proof

      let V be RealUnitarySpace;

      let x,y be VECTOR of V;

      

       A1: (x .|. x) >= 0 by BHSP_1:def 2;

       ||.(x + y).|| = ( sqrt ((x + y) .|. (x + y))) by BHSP_1:def 4;

      then

       A2: ( sqrt ( ||.(x + y).|| ^2 )) = ( sqrt ((x + y) .|. (x + y))) by BHSP_1: 28, SQUARE_1: 22;

      

       A3: (y .|. y) >= 0 by BHSP_1:def 2;

      ((x + y) .|. (x + y)) >= 0 & ( ||.(x + y).|| ^2 ) >= 0 by BHSP_1:def 2, XREAL_1: 63;

      

      then ( ||.(x + y).|| ^2 ) = ((x + y) .|. (x + y)) by A2, SQUARE_1: 28

      .= (((x .|. x) + (2 * (x .|. y))) + (y .|. y)) by BHSP_1: 16

      .= (((( sqrt (x .|. x)) ^2 ) + (2 * (x .|. y))) + (y .|. y)) by A1, SQUARE_1:def 2

      .= ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + (y .|. y)) by BHSP_1:def 4

      .= ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + (( sqrt (y .|. y)) ^2 )) by A3, SQUARE_1:def 2;

      hence ( ||.(x + y).|| ^2 ) = ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) by BHSP_1:def 4;

       ||.(x - y).|| = ( sqrt ((x - y) .|. (x - y))) by BHSP_1:def 4;

      then

       A4: ( sqrt ( ||.(x - y).|| ^2 )) = ( sqrt ((x - y) .|. (x - y))) by BHSP_1: 28, SQUARE_1: 22;

      ((x - y) .|. (x - y)) >= 0 & ( ||.(x - y).|| ^2 ) >= 0 by BHSP_1:def 2, XREAL_1: 63;

      

      then ( ||.(x - y).|| ^2 ) = ((x - y) .|. (x - y)) by A4, SQUARE_1: 28

      .= (((x .|. x) - (2 * (x .|. y))) + (y .|. y)) by BHSP_1: 18

      .= (((( sqrt (x .|. x)) ^2 ) - (2 * (x .|. y))) + (y .|. y)) by A1, SQUARE_1:def 2

      .= ((( ||.x.|| ^2 ) - (2 * (x .|. y))) + (y .|. y)) by BHSP_1:def 4

      .= ((( ||.x.|| ^2 ) - (2 * (x .|. y))) + (( sqrt (y .|. y)) ^2 )) by A3, SQUARE_1:def 2;

      hence thesis by BHSP_1:def 4;

    end;

    theorem :: RUSUB_5:30

    for V be RealUnitarySpace, x,y be VECTOR of V st (x,y) are_orthogonal holds ( ||.(x + y).|| ^2 ) = (( ||.x.|| ^2 ) + ( ||.y.|| ^2 ))

    proof

      let V be RealUnitarySpace;

      let x,y be VECTOR of V;

      assume (x,y) are_orthogonal ;

      then

       A1: (x .|. y) = 0 by BHSP_1:def 3;

      ( ||.(x + y).|| ^2 ) = ((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) by Th29;

      hence thesis by A1;

    end;

    theorem :: RUSUB_5:31

    for V be RealUnitarySpace, x,y be VECTOR of V holds (( ||.(x + y).|| ^2 ) + ( ||.(x - y).|| ^2 )) = ((2 * ( ||.x.|| ^2 )) + (2 * ( ||.y.|| ^2 )))

    proof

      let V be RealUnitarySpace;

      let x,y be VECTOR of V;

      (( ||.(x + y).|| ^2 ) + ( ||.(x - y).|| ^2 )) = (((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) + ( ||.(x - y).|| ^2 )) by Th29

      .= (((( ||.x.|| ^2 ) + (2 * (x .|. y))) + ( ||.y.|| ^2 )) + ((( ||.x.|| ^2 ) - (2 * (x .|. y))) + ( ||.y.|| ^2 ))) by Th29

      .= ((( ||.x.|| ^2 ) + ( ||.x.|| ^2 )) + (2 * ( ||.y.|| ^2 )));

      hence thesis;

    end;

    theorem :: RUSUB_5:32

    for V be RealUnitarySpace, v be VECTOR of V holds ex W be Subspace of V st the carrier of W = { u where u be VECTOR of V : (u .|. v) = 0 }

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      set M = { u where u be VECTOR of V : (u .|. v) = 0 };

      for x be object st x in M holds x in the carrier of V

      proof

        let x be object;

        assume x in M;

        then ex u be VECTOR of V st x = u & (u .|. v) = 0 ;

        hence thesis;

      end;

      then

      reconsider M as Subset of V by TARSKI:def 3;

      (( 0. V) .|. v) = 0 by BHSP_1: 14;

      then

       A1: ( 0. V) in M;

      then

      reconsider M as non empty Subset of V;

      for x,y be VECTOR of V, a be Real st x in M & y in M holds (((1 - a) * x) + (a * y)) in M

      proof

        let x,y be VECTOR of V;

        let a be Real;

        assume that

         A2: x in M and

         A3: y in M;

        consider u2 be VECTOR of V such that

         A4: y = u2 and

         A5: (u2 .|. v) = 0 by A3;

        consider u1 be VECTOR of V such that

         A6: x = u1 and

         A7: (u1 .|. v) = 0 by A2;

        ((((1 - a) * u1) + (a * u2)) .|. v) = ((((1 - a) * u1) .|. v) + ((a * u2) .|. v)) by BHSP_1:def 2

        .= (((1 - a) * (u1 .|. v)) + ((a * u2) .|. v)) by BHSP_1:def 2

        .= (a * 0 ) by A7, A5, BHSP_1:def 2;

        hence thesis by A6, A4;

      end;

      then

      reconsider M as non empty Affine Subset of V by RUSUB_4:def 4;

      take ( Lin M);

      thus thesis by A1, RUSUB_4: 28;

    end;

    begin

    definition

      let V be RealUnitarySpace;

      :: RUSUB_5:def5

      func Family_open_set (V) -> Subset-Family of V means

      : Def5: for M be Subset of V holds M in it iff for x be Point of V st x in M holds ex r be Real st r > 0 & ( Ball (x,r)) c= M;

      existence

      proof

        defpred P[ Subset of V] means for x be Point of V st x in $1 holds ex r be Real st r > 0 & ( Ball (x,r)) c= $1;

        ex F be Subset-Family of V st for M be Subset of V holds M in F iff P[M] from SUBSET_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let FX,GX be Subset-Family of V;

        assume

         A1: for M be Subset of V holds M in FX iff for x be Point of V st x in M holds ex r be Real st r > 0 & ( Ball (x,r)) c= M;

        assume

         A2: for N be Subset of V holds N in GX iff for y be Point of V st y in N holds ex p be Real st p > 0 & ( Ball (y,p)) c= N;

        for Y be Subset of V holds Y in FX iff Y in GX

        proof

          let Y be Subset of V;

           A3:

          now

            assume Y in GX;

            then for x be Point of V st x in Y holds ex r be Real st r > 0 & ( Ball (x,r)) c= Y by A2;

            hence Y in FX by A1;

          end;

          now

            assume Y in FX;

            then for x be Point of V st x in Y holds ex r be Real st r > 0 & ( Ball (x,r)) c= Y by A1;

            hence Y in GX by A2;

          end;

          hence thesis by A3;

        end;

        hence thesis by SETFAM_1: 31;

      end;

    end

    theorem :: RUSUB_5:33

    

     Th33: for V be RealUnitarySpace, v be Point of V, r,p be Real st r <= p holds ( Ball (v,r)) c= ( Ball (v,p))

    proof

      let V be RealUnitarySpace;

      let v be Point of V;

      let r,p be Real;

      assume

       A1: r <= p;

      for u be Point of V st u in ( Ball (v,r)) holds u in ( Ball (v,p))

      proof

        let u be Point of V;

        assume u in ( Ball (v,r));

        then ( dist (v,u)) < r by BHSP_2: 41;

        then (( dist (v,u)) + r) < (r + p) by A1, XREAL_1: 8;

        then ( dist (v,u)) < ((r + p) - r) by XREAL_1: 20;

        hence thesis by BHSP_2: 41;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_5:34

    

     Th34: for V be RealUnitarySpace, v be Point of V holds ex r be Real st r > 0 & ( Ball (v,r)) c= the carrier of V

    proof

      let V be RealUnitarySpace;

      let v be Point of V;

      take r = 1;

      thus r > 0 ;

      thus thesis;

    end;

    theorem :: RUSUB_5:35

    

     Th35: for V be RealUnitarySpace, v,u be Point of V, r be Real st u in ( Ball (v,r)) holds ex p be Real st p > 0 & ( Ball (u,p)) c= ( Ball (v,r))

    proof

      let V be RealUnitarySpace;

      let v,u be Point of V;

      let r be Real;

      assume u in ( Ball (v,r));

      then

       A1: ( dist (v,u)) < r by BHSP_2: 41;

      thus thesis

      proof

        set p = (r - ( dist (v,u)));

        take p;

        thus p > 0 by A1, XREAL_1: 50;

        for w be Point of V holds w in ( Ball (u,p)) implies w in ( Ball (v,r))

        proof

          let w be Point of V;

          assume w in ( Ball (u,p));

          then ( dist (u,w)) < (r - ( dist (v,u))) by BHSP_2: 41;

          then

           A2: (( dist (v,u)) + ( dist (u,w))) < r by XREAL_1: 20;

          (( dist (v,u)) + ( dist (u,w))) >= ( dist (v,w)) by BHSP_1: 35;

          then ( dist (v,w)) < r by A2, XXREAL_0: 2;

          hence thesis by BHSP_2: 41;

        end;

        hence thesis;

      end;

    end;

    theorem :: RUSUB_5:36

    for V be RealUnitarySpace, u,v,w be Point of V, r,p be Real st v in (( Ball (u,r)) /\ ( Ball (w,p))) holds ex q be Real st ( Ball (v,q)) c= ( Ball (u,r)) & ( Ball (v,q)) c= ( Ball (w,p))

    proof

      let V be RealUnitarySpace;

      let u,v,w be Point of V;

      let r,p be Real;

      assume

       A1: v in (( Ball (u,r)) /\ ( Ball (w,p)));

      then v in ( Ball (u,r)) by XBOOLE_0:def 4;

      then

      consider s be Real such that s > 0 and

       A2: ( Ball (v,s)) c= ( Ball (u,r)) by Th35;

      v in ( Ball (w,p)) by A1, XBOOLE_0:def 4;

      then

      consider t be Real such that t > 0 and

       A3: ( Ball (v,t)) c= ( Ball (w,p)) by Th35;

      take q = ( min (s,t));

      ( Ball (v,q)) c= ( Ball (v,s)) by Th33, XXREAL_0: 17;

      hence ( Ball (v,q)) c= ( Ball (u,r)) by A2;

      ( Ball (v,q)) c= ( Ball (v,t)) by Th33, XXREAL_0: 17;

      hence thesis by A3;

    end;

    theorem :: RUSUB_5:37

    

     Th37: for V be RealUnitarySpace, v be Point of V, r be Real holds ( Ball (v,r)) in ( Family_open_set V)

    proof

      let V be RealUnitarySpace;

      let v be Point of V;

      let r be Real;

      for u be Point of V st u in ( Ball (v,r)) holds ex p be Real st p > 0 & ( Ball (u,p)) c= ( Ball (v,r)) by Th35;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_5:38

    

     Th38: for V be RealUnitarySpace holds the carrier of V in ( Family_open_set V)

    proof

      let V be RealUnitarySpace;

      the carrier of V c= the carrier of V & for v be Point of V st v in the carrier of V holds ex p be Real st p > 0 & ( Ball (v,p)) c= the carrier of V by Th34;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_5:39

    

     Th39: for V be RealUnitarySpace, M,N be Subset of V st M in ( Family_open_set V) & N in ( Family_open_set V) holds (M /\ N) in ( Family_open_set V)

    proof

      let V be RealUnitarySpace;

      let M,N be Subset of V;

      assume that

       A1: M in ( Family_open_set V) and

       A2: N in ( Family_open_set V);

      for v be Point of V st v in (M /\ N) holds ex q be Real st q > 0 & ( Ball (v,q)) c= (M /\ N)

      proof

        let v be Point of V;

        assume

         A3: v in (M /\ N);

        then v in M by XBOOLE_0:def 4;

        then

        consider p be Real such that

         A4: p > 0 and

         A5: ( Ball (v,p)) c= M by A1, Def5;

        v in N by A3, XBOOLE_0:def 4;

        then

        consider r be Real such that

         A6: r > 0 and

         A7: ( Ball (v,r)) c= N by A2, Def5;

        take q = ( min (p,r));

        thus q > 0 by A4, A6, XXREAL_0: 15;

        ( Ball (v,q)) c= ( Ball (v,r)) by Th33, XXREAL_0: 17;

        then

         A8: ( Ball (v,q)) c= N by A7;

        ( Ball (v,q)) c= ( Ball (v,p)) by Th33, XXREAL_0: 17;

        then ( Ball (v,q)) c= M by A5;

        hence thesis by A8, XBOOLE_1: 19;

      end;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_5:40

    

     Th40: for V be RealUnitarySpace, A be Subset-Family of V st A c= ( Family_open_set V) holds ( union A) in ( Family_open_set V)

    proof

      let V be RealUnitarySpace;

      let A be Subset-Family of V;

      assume

       A1: A c= ( Family_open_set V);

      for x be Point of V st x in ( union A) holds ex r be Real st r > 0 & ( Ball (x,r)) c= ( union A)

      proof

        let x be Point of V;

        assume x in ( union A);

        then

        consider W be set such that

         A2: x in W and

         A3: W in A by TARSKI:def 4;

        reconsider W as Subset of V by A3;

        consider r be Real such that

         A4: r > 0 and

         A5: ( Ball (x,r)) c= W by A1, A2, A3, Def5;

        take r;

        thus r > 0 by A4;

        W c= ( union A) by A3, ZFMISC_1: 74;

        hence thesis by A5;

      end;

      hence thesis by Def5;

    end;

    theorem :: RUSUB_5:41

    

     Th41: for V be RealUnitarySpace holds TopStruct (# the carrier of V, ( Family_open_set V) #) is TopSpace

    proof

      let V be RealUnitarySpace;

      set T = TopStruct (# the carrier of V, ( Family_open_set V) #);

      

       A1: for p,q be Subset of T st p in the topology of T & q in the topology of T holds (p /\ q) in the topology of T by Th39;

      the carrier of T in the topology of T & for a be Subset-Family of T st a c= the topology of T holds ( union a) in the topology of T by Th38, Th40;

      hence thesis by A1, PRE_TOPC:def 1;

    end;

    definition

      let V be RealUnitarySpace;

      :: RUSUB_5:def6

      func TopUnitSpace V -> TopStruct equals TopStruct (# the carrier of V, ( Family_open_set V) #);

      coherence ;

    end

    registration

      let V be RealUnitarySpace;

      cluster ( TopUnitSpace V) -> TopSpace-like;

      coherence by Th41;

    end

    registration

      let V be RealUnitarySpace;

      cluster ( TopUnitSpace V) -> non empty;

      coherence ;

    end

    theorem :: RUSUB_5:42

    for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V) st M = ( [#] V) holds M is open & M is closed

    proof

      let V be RealUnitarySpace;

      let M be Subset of ( TopUnitSpace V);

      

       A1: ( [#] ( TopUnitSpace V)) = the carrier of TopStruct (# the carrier of V, ( Family_open_set V) #);

      assume M = ( [#] V);

      hence thesis by A1;

    end;

    theorem :: RUSUB_5:43

    for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V) st M = ( {} V) holds M is open & M is closed;

    theorem :: RUSUB_5:44

    for V be RealUnitarySpace, v be VECTOR of V, r be Real st the carrier of V = {( 0. V)} & r <> 0 holds ( Sphere (v,r)) is empty

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let r be Real;

      assume that

       A1: the carrier of V = {( 0. V)} and

       A2: r <> 0 ;

      assume ( Sphere (v,r)) is non empty;

      then

      consider x be object such that

       A3: x in ( Sphere (v,r));

      ( Sphere (v,r)) = { y where y be Point of V : ||.(v - y).|| = r } by BHSP_2:def 7;

      then

      consider w be Point of V such that x = w and

       A4: ||.(v - w).|| = r by A3;

      (v - w) <> ( 0. V) by A2, A4, BHSP_1: 26;

      hence contradiction by A1, TARSKI:def 1;

    end;

    theorem :: RUSUB_5:45

    for V be RealUnitarySpace, v be VECTOR of V, r be Real st the carrier of V <> {( 0. V)} & r > 0 holds ( Sphere (v,r)) is non empty

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let r be Real;

      assume that

       A1: the carrier of V <> {( 0. V)} and

       A2: r > 0 ;

      now

        per cases ;

          suppose

           A3: v = ( 0. V);

          ex u be VECTOR of V st u <> ( 0. V)

          proof

             not the carrier of V c= {( 0. V)} by A1;

            then ( NonZero V) <> {} by XBOOLE_1: 37;

            then

            consider u be object such that

             A4: u in ( NonZero V) by XBOOLE_0:def 1;

            

             A5: not u in {( 0. V)} by A4, XBOOLE_0:def 5;

            reconsider u as VECTOR of V by A4;

            take u;

            thus thesis by A5, TARSKI:def 1;

          end;

          then

          consider u be VECTOR of V such that

           A6: u <> ( 0. V);

          set a = ||.u.||;

          

           A7: a <> 0 by A6, BHSP_1: 26;

          set u9 = ((r * (1 / a)) * u);

          

           A8: a >= 0 by BHSP_1: 28;

           ||.(v - u9).|| = ||.( - ((r * (1 / a)) * u)).|| by A3

          .= ||.((r * (1 / a)) * u).|| by BHSP_1: 31

          .= ( |.(r * (1 / a)).| * ||.u.||) by BHSP_1: 27;

          

          then ||.(v - u9).|| = ((r * (1 / a)) * ||.u.||) by A2, A8, ABSVALUE:def 1

          .= r by A7, XCMPLX_1: 109;

          then u9 in { y where y be Point of V : ||.(v - y).|| = r };

          hence thesis by BHSP_2:def 7;

        end;

          suppose

           A9: v <> ( 0. V);

          set a = ||.v.||;

          

           A10: a <> 0 by A9, BHSP_1: 26;

          set u9 = ((1 - (r / a)) * v);

          

           A11: ||.(v - u9).|| = ||.((1 * v) - ((1 - (r / a)) * v)).|| by RLVECT_1:def 8

          .= ||.((1 - (1 - (r / a))) * v).|| by RLVECT_1: 35

          .= ( |.(r / a).| * ||.v.||) by BHSP_1: 27;

          a >= 0 by BHSP_1: 28;

          

          then ||.(v - u9).|| = ((r / a) * a) by A2, A11, ABSVALUE:def 1

          .= (r / (a / a)) by XCMPLX_1: 81

          .= r by A10, XCMPLX_1: 51;

          then u9 in { y where y be Point of V : ||.(v - y).|| = r };

          hence thesis by BHSP_2:def 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_5:46

    for V be RealUnitarySpace, v be VECTOR of V, r be Real st r = 0 holds ( Ball (v,r)) is empty

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: r = 0 ;

      assume ( Ball (v,r)) is non empty;

      then

      consider u be object such that

       A2: u in ( Ball (v,r));

      u in { y where y be Point of V : ||.(v - y).|| < r } by A2, BHSP_2:def 5;

      then ex w be Point of V st u = w & ||.(v - w).|| < r;

      hence contradiction by A1, BHSP_1: 28;

    end;

    theorem :: RUSUB_5:47

    for V be RealUnitarySpace, v be VECTOR of V, r be Real st the carrier of V = {( 0. V)} & r > 0 holds ( Ball (v,r)) = {( 0. V)}

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let r be Real;

      assume that

       A1: the carrier of V = {( 0. V)} and

       A2: r > 0 ;

      for w be VECTOR of V st w in {( 0. V)} holds w in ( Ball (v,r))

      proof

        let w be VECTOR of V;

        assume

         A3: w in {( 0. V)};

        v = ( 0. V) by A1, TARSKI:def 1;

        

        then ||.(v - w).|| = ||.(( 0. V) - ( 0. V)).|| by A3, TARSKI:def 1

        .= ||.( 0. V).||

        .= 0 by BHSP_1: 26;

        then w in { y where y be Point of V : ||.(v - y).|| < r } by A2;

        hence thesis by BHSP_2:def 5;

      end;

      then {( 0. V)} c= ( Ball (v,r));

      hence thesis by A1;

    end;

    theorem :: RUSUB_5:48

    for V be RealUnitarySpace, v be VECTOR of V, r be Real st the carrier of V <> {( 0. V)} & r > 0 holds ex w be VECTOR of V st w <> v & w in ( Ball (v,r))

    proof

      let V be RealUnitarySpace;

      let v be VECTOR of V;

      let r be Real;

      assume that

       A1: the carrier of V <> {( 0. V)} and

       A2: r > 0 ;

      consider r9 be Real such that

       A3: 0 < r9 and

       A4: r9 < r by A2, XREAL_1: 5;

      reconsider r9 as Real;

      now

        per cases ;

          suppose

           A5: v = ( 0. V);

          ex w be VECTOR of V st w <> ( 0. V) & ||.w.|| < r

          proof

             not the carrier of V c= {( 0. V)} by A1;

            then ( NonZero V) <> {} by XBOOLE_1: 37;

            then

            consider u be object such that

             A6: u in ( NonZero V) by XBOOLE_0:def 1;

            

             A7: not u in {( 0. V)} by A6, XBOOLE_0:def 5;

            reconsider u as VECTOR of V by A6;

            

             A8: u <> ( 0. V) by A7, TARSKI:def 1;

            then

             A9: ||.u.|| <> 0 by BHSP_1: 26;

            set a = ||.u.||;

            

             A10: ||.u.|| >= 0 by BHSP_1: 28;

            take w = ((r9 / a) * u);

            

             A11: ||.w.|| = ( |.(r9 / a).| * ||.u.||) by BHSP_1: 27

            .= ((r9 / a) * ||.u.||) by A3, A10, ABSVALUE:def 1

            .= (r9 / (a / a)) by XCMPLX_1: 81

            .= r9 by A9, XCMPLX_1: 51;

            (r9 / a) > 0 by A3, A9, A10, XREAL_1: 139;

            hence thesis by A4, A8, A11, RLVECT_1: 11;

          end;

          then

          consider u be VECTOR of V such that

           A12: u <> ( 0. V) and

           A13: ||.u.|| < r;

           ||.(v - u).|| = ||.( - u).|| by A5

          .= ||.u.|| by BHSP_1: 31;

          then u in { y where y be Point of V : ||.(v - y).|| < r } by A13;

          then u in ( Ball (v,r)) by BHSP_2:def 5;

          hence thesis by A5, A12;

        end;

          suppose

           A14: v <> ( 0. V);

          set a = ||.v.||;

          

           A15: a <> 0 by A14, BHSP_1: 26;

          set u9 = ((1 - (r9 / a)) * v);

          

           A16: ||.(v - u9).|| = ||.((1 * v) - ((1 - (r9 / a)) * v)).|| by RLVECT_1:def 8

          .= ||.((1 - (1 - (r9 / a))) * v).|| by RLVECT_1: 35

          .= ( |.(r9 / a).| * ||.v.||) by BHSP_1: 27;

          a >= 0 by BHSP_1: 28;

          

          then

           A17: ||.(v - u9).|| = ((r9 / a) * a) by A3, A16, ABSVALUE:def 1

          .= (r9 / (a / a)) by XCMPLX_1: 81

          .= r9 by A15, XCMPLX_1: 51;

          then (v - u9) <> ( 0. V) by A3, BHSP_1: 26;

          then

           A18: v <> u9 by RLVECT_1: 15;

          u9 in { y where y be Point of V : ||.(v - y).|| < r } by A4, A17;

          then u9 in ( Ball (v,r)) by BHSP_2:def 5;

          hence thesis by A18;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_5:49

    for V be RealUnitarySpace holds the carrier of V = the carrier of ( TopUnitSpace V) & the topology of ( TopUnitSpace V) = ( Family_open_set V);

    theorem :: RUSUB_5:50

    

     Th50: for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V), r be Real, v be Point of V st M = ( Ball (v,r)) holds M is open by Th37;

    theorem :: RUSUB_5:51

    for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V) holds M is open iff for v be Point of V st v in M holds ex r be Real st r > 0 & ( Ball (v,r)) c= M by Def5;

    theorem :: RUSUB_5:52

    for V be RealUnitarySpace, v1,v2 be Point of V, r1,r2 be Real holds ex u be Point of V, r be Real st (( Ball (v1,r1)) \/ ( Ball (v2,r2))) c= ( Ball (u,r))

    proof

      let V be RealUnitarySpace;

      let v1,v2 be Point of V;

      let r1,r2 be Real;

      reconsider u = v1 as Point of V;

      reconsider r = (( |.r1.| + |.r2.|) + ( dist (v1,v2))) as Real;

      take u;

      take r;

      let a be object;

      assume

       A1: a in (( Ball (v1,r1)) \/ ( Ball (v2,r2)));

      then

      reconsider a as Point of V;

      now

        per cases by A1, XBOOLE_0:def 3;

          case a in ( Ball (v1,r1));

          then

           A2: ( dist (u,a)) < r1 by BHSP_2: 41;

          r1 <= |.r1.| & 0 <= |.r2.| by ABSVALUE: 4, COMPLEX1: 46;

          then

           A3: (r1 + 0 ) <= ( |.r1.| + |.r2.|) by XREAL_1: 7;

           0 <= ( dist (v1,v2)) by BHSP_1: 37;

          then (r1 + 0 ) <= (( |.r1.| + |.r2.|) + ( dist (v1,v2))) by A3, XREAL_1: 7;

          then (( dist (u,a)) - r) < (r1 - r1) by A2, XREAL_1: 14;

          then ((( dist (u,a)) - r) + r) < ( 0 + r) by XREAL_1: 8;

          hence thesis by BHSP_2: 41;

        end;

          case a in ( Ball (v2,r2));

          then ( dist (v2,a)) < r2 by BHSP_2: 41;

          then (( dist (v2,a)) - |.r2.|) < (r2 - r2) by ABSVALUE: 4, XREAL_1: 14;

          then ((( dist (v2,a)) - |.r2.|) + |.r2.|) < ( 0 + |.r2.|) by XREAL_1: 8;

          then (( dist (u,a)) - |.r2.|) < ((( dist (v1,v2)) + ( dist (v2,a))) - ( dist (v2,a))) by BHSP_1: 35, XREAL_1: 15;

          then ((( dist (u,a)) - |.r2.|) - |.r1.|) < (( dist (v1,v2)) - 0 ) by COMPLEX1: 46, XREAL_1: 14;

          then ((( dist (u,a)) - ( |.r1.| + |.r2.|)) + ( |.r1.| + |.r2.|)) < (( |.r1.| + |.r2.|) + ( dist (v1,v2))) by XREAL_1: 8;

          hence thesis by BHSP_2: 41;

        end;

      end;

      hence thesis;

    end;

    theorem :: RUSUB_5:53

    

     Th53: for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V), v be VECTOR of V, r be Real st M = ( cl_Ball (v,r)) holds M is closed

    proof

      let V be RealUnitarySpace;

      let M be Subset of ( TopUnitSpace V);

      let v be VECTOR of V;

      let r be Real;

      assume

       A1: M = ( cl_Ball (v,r));

      for x be set holds x in (M ` ) iff ex Q be Subset of ( TopUnitSpace V) st Q is open & Q c= (M ` ) & x in Q

      proof

        let x be set;

        thus x in (M ` ) implies ex Q be Subset of ( TopUnitSpace V) st Q is open & Q c= (M ` ) & x in Q

        proof

          assume

           A2: x in (M ` );

          then

          reconsider e = x as Point of V;

          reconsider Q = ( Ball (e,(( dist (e,v)) - r))) as Subset of ( TopUnitSpace V);

          take Q;

          thus Q is open by Th50;

          thus Q c= (M ` )

          proof

            let q be object;

            assume

             A3: q in Q;

            then

            reconsider f = q as Point of V;

            ( dist (e,v)) <= (( dist (e,f)) + ( dist (f,v))) by BHSP_1: 35;

            then

             A4: (( dist (e,v)) - r) <= ((( dist (e,f)) + ( dist (f,v))) - r) by XREAL_1: 9;

            ( dist (e,f)) < (( dist (e,v)) - r) by A3, BHSP_2: 41;

            then ( dist (e,f)) < ((( dist (e,f)) + ( dist (f,v))) - r) by A4, XXREAL_0: 2;

            then (( dist (e,f)) - ( dist (e,f))) < (((( dist (e,f)) + ( dist (f,v))) - r) - ( dist (e,f))) by XREAL_1: 9;

            then 0 < (((( dist (e,f)) - ( dist (e,f))) + ( dist (f,v))) - r);

            then ( dist (f,v)) > r by XREAL_1: 47;

            then not q in M by A1, BHSP_2: 48;

            hence thesis by A3, SUBSET_1: 29;

          end;

           not x in M by A2, XBOOLE_0:def 5;

          then ( dist (v,e)) > r by A1, BHSP_2: 48;

          then (( dist (e,v)) - r) > (r - r) by XREAL_1: 9;

          hence thesis by BHSP_2: 42;

        end;

        thus thesis;

      end;

      then (M ` ) is open by TOPS_1: 25;

      hence thesis;

    end;

    theorem :: RUSUB_5:54

    for V be RealUnitarySpace, M be Subset of ( TopUnitSpace V), v be VECTOR of V, r be Real st M = ( Sphere (v,r)) holds M is closed

    proof

      let V be RealUnitarySpace;

      let M be Subset of ( TopUnitSpace V);

      let v be VECTOR of V;

      let r be Real;

      reconsider B = ( cl_Ball (v,r)), C = ( Ball (v,r)) as Subset of ( TopUnitSpace V);

      assume

       A1: M = ( Sphere (v,r));

      

       A2: (M ` ) = ((B ` ) \/ C)

      proof

        hereby

          let a be object;

          assume

           A3: a in (M ` );

          then

          reconsider e = a as Point of V;

           not a in M by A3, XBOOLE_0:def 5;

          then ( dist (e,v)) <> r by A1, BHSP_2: 52;

          then ( dist (e,v)) < r or ( dist (e,v)) > r by XXREAL_0: 1;

          then e in ( Ball (v,r)) or not e in ( cl_Ball (v,r)) by BHSP_2: 41, BHSP_2: 48;

          then e in ( Ball (v,r)) or e in (( cl_Ball (v,r)) ` ) by SUBSET_1: 29;

          hence a in ((B ` ) \/ C) by XBOOLE_0:def 3;

        end;

        let a be object;

        assume

         A4: a in ((B ` ) \/ C);

        then

        reconsider e = a as Point of V;

        a in (B ` ) or a in C by A4, XBOOLE_0:def 3;

        then not e in ( cl_Ball (v,r)) or e in C by XBOOLE_0:def 5;

        then ( dist (e,v)) > r or ( dist (e,v)) < r by BHSP_2: 41, BHSP_2: 48;

        then not a in M by A1, BHSP_2: 52;

        hence thesis by A4, SUBSET_1: 29;

      end;

      B is closed & C is open by Th50, Th53;

      hence thesis by A2;

    end;