:: ANALORT semantic presentation

definition
let c1 be non empty Abelian LoopStr ;
let c2, c3 be Element of c1;
redefine func + as a2 + a3 -> M3(the carrier of a1);
commutativity
for b1, b2 being Element of c1 holds b1 + b2 = b2 + b1 by RLVECT_1:def 5;
end;

E1: for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6, b7, b8, b9 being Real holds
( ( b2 = (b6 * b3) + (b7 * b4) & b5 = (b8 * b3) + (b9 * b4) ) implies ( ( b2 + b5 = ((b6 + b8) * b3) + ((b7 + b9) * b4) & b2 - b5 = ((b6 - b8) * b3) + ((b7 - b9) * b4) ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6, c7, c8, c9 be Real;
assume that E2: c2 = (c6 * c3) + (c7 * c4)
and E3: c5 = (c8 * c3) + (c9 * c4) ;
thus c2 + c5 = (((c6 * c3) + (c7 * c4)) + (c8 * c3)) + (c9 * c4) by E2, E3, RLVECT_1:def 6
.= (((c6 * c3) + (c8 * c3)) + (c7 * c4)) + (c9 * c4) by RLVECT_1:def 6
.= (((c6 + c8) * c3) + (c7 * c4)) + (c9 * c4) by RLVECT_1:def 9
.= ((c6 + c8) * c3) + ((c7 * c4) + (c9 * c4)) by RLVECT_1:def 6
.= ((c6 + c8) * c3) + ((c7 + c9) * c4) by RLVECT_1:def 9 ;
thus c2 - c5 = ((c6 * c3) + (c7 * c4)) + (- ((c8 * c3) + (c9 * c4))) by E2, E3, RLVECT_1:def 11
.= ((c6 * c3) + (c7 * c4)) + ((- (c8 * c3)) + (- (c9 * c4))) by RLVECT_1:45
.= ((c6 * c3) + (c7 * c4)) + ((c8 * (- c3)) + (- (c9 * c4))) by RLVECT_1:39
.= ((c6 * c3) + (c7 * c4)) + ((c8 * (- c3)) + (c9 * (- c4))) by RLVECT_1:39
.= ((c6 * c3) + (c7 * c4)) + (((- c8) * c3) + (c9 * (- c4))) by RLVECT_1:38
.= ((c6 * c3) + (c7 * c4)) + (((- c8) * c3) + ((- c9) * c4)) by RLVECT_1:38
.= (((c6 * c3) + (c7 * c4)) + ((- c8) * c3)) + ((- c9) * c4) by RLVECT_1:def 6
.= (((c6 * c3) + ((- c8) * c3)) + (c7 * c4)) + ((- c9) * c4) by RLVECT_1:def 6
.= (((c6 + (- c8)) * c3) + (c7 * c4)) + ((- c9) * c4) by RLVECT_1:def 9
.= ((c6 + (- c8)) * c3) + ((c7 * c4) + ((- c9) * c4)) by RLVECT_1:def 6
.= ((c6 - c8) * c3) + ((c7 + (- c9)) * c4) by RLVECT_1:def 9
.= ((c6 - c8) * c3) + ((c7 - c9) * c4) ;
end;

E2: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1
for b5, b6, b7 being Real holds
( b2 = (b5 * b3) + (b6 * b4) implies b7 * b2 = ((b7 * b5) * b3) + ((b7 * b6) * b4) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
let c5, c6, c7 be Real;
assume c2 = (c5 * c3) + (c6 * c4) ;
hence c7 * c2 = (c7 * (c5 * c3)) + (c7 * (c6 * c4)) by RLVECT_1:def 9
.= ((c7 * c5) * c3) + (c7 * (c6 * c4)) by RLVECT_1:def 9
.= ((c7 * c5) * c3) + ((c7 * c6) * c4) by RLVECT_1:def 9 ;

end;

E3: for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1
for b4, b5, b6, b7 being Real holds
( ( Gen b2,b3 & (b4 * b2) + (b5 * b3) = (b6 * b2) + (b7 * b3) ) implies ( ( b4 = b6 & b5 = b7 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
let c4, c5, c6, c7 be Real;
assume that E4: Gen c2,c3
and E5: (c4 * c2) + (c5 * c3) = (c6 * c2) + (c7 * c3) ;
0. c1 = ((c4 * c2) + (c5 * c3)) - ((c6 * c2) + (c7 * c3)) by E5, RLVECT_1:28
.= ((c4 - c6) * c2) + ((c5 - c7) * c3) by E1 ;
then ( (- c6) + c4 = 0 & (- c7) + c5 = 0 ) by E4, ANALMETR:def 1;
then ( c4 = - (- c6) & c5 = - (- c7) ) ;
hence ( c4 = c6 & c5 = c7 ) ;
end;

E4: for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 implies ( b2 <> 0. b1 & b3 <> 0. b1 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E5: Gen c2,c3 ;
E6: c2 <> 0. c1
proof
assume E7: c2 = 0. c1 ;
consider c4, c5 being Real such that
E8: c4 = 1
and E9: c5 = 0 ;
(c4 * c2) + (c5 * c3) = (0. c1) + (0 * c3) by E7, E9, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
hence not verum by E5, E8, ANALMETR:def 1;
end;
c3 <> 0. c1
proof
assume E7: c3 = 0. c1 ;
consider c4, c5 being Real such that
E8: c4 = 0
and E9: c5 = 1 ;
(c4 * c2) + (c5 * c3) = (0. c1) + (1 * (0. c1)) by E7, E8, E9, RLVECT_1:23
.= (0. c1) + (0. c1) by RLVECT_1:23
.= 0. c1 by RLVECT_1:10 ;
hence not verum by E5, E9, ANALMETR:def 1;
end;
hence ( c2 <> 0. c1 & c3 <> 0. c1 ) by E6;
end;

E5: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( Gen b2,b3 implies b4 = ((pr1 b2,b3,b4) * b2) + ((pr2 b2,b3,b4) * b3) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume E6: Gen c2,c3 ;
then ex b1 being Real st c4 = ((pr1 c2,c3,c4) * c2) + (b1 * c3) by GEOMTRAP:def 4;
hence c4 = ((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * c3) by E6, GEOMTRAP:def 5;
end;

E6: for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1
for b5, b6 being Real holds
( ( Gen b2,b3 & b4 = (b5 * b2) + (b6 * b3) ) implies ( ( b5 = pr1 b2,b3,b4 & b6 = pr2 b2,b3,b4 ) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
let c5, c6 be Real;
assume E7: ( Gen c2,c3 & c4 = (c5 * c2) + (c6 * c3) ) ;
then c4 = ((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * c3) by E5;
hence ( c5 = pr1 c2,c3,c4 & c6 = pr2 c2,c3,c4 ) by E7, E3;
end;

E7: for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1
for b6 being Real holds
( Gen b2,b3 implies ( pr1 b2,b3,(b4 + b5) = (pr1 b2,b3,b4) + (pr1 b2,b3,b5) & pr2 b2,b3,(b4 + b5) = (pr2 b2,b3,b4) + (pr2 b2,b3,b5) & pr1 b2,b3,(b4 - b5) = (pr1 b2,b3,b4) - (pr1 b2,b3,b5) & pr2 b2,b3,(b4 - b5) = (pr2 b2,b3,b4) - (pr2 b2,b3,b5) & pr1 b2,b3,(b6 * b4) = b6 * (pr1 b2,b3,b4) & pr2 b2,b3,(b6 * b4) = b6 * (pr2 b2,b3,b4) ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
let c6 be Real;
assume E8: Gen c2,c3 ;
set c7 = pr1 c2,c3,c4;
set c8 = pr2 c2,c3,c4;
set c9 = pr1 c2,c3,c5;
set c10 = pr2 c2,c3,c5;
E9: ( c4 = ((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * c3) & c5 = ((pr1 c2,c3,c5) * c2) + ((pr2 c2,c3,c5) * c3) ) by E8, E5;
then c4 + c5 = ((((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * c3)) + ((pr1 c2,c3,c5) * c2)) + ((pr2 c2,c3,c5) * c3) by RLVECT_1:def 6
.= ((((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + ((pr2 c2,c3,c4) * c3)) + ((pr2 c2,c3,c5) * c3) by RLVECT_1:def 6
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + (((pr2 c2,c3,c4) * c3) + ((pr2 c2,c3,c5) * c3)) by RLVECT_1:def 6
.= (((pr1 c2,c3,c4) + (pr1 c2,c3,c5)) * c2) + (((pr2 c2,c3,c4) * c3) + ((pr2 c2,c3,c5) * c3)) by RLVECT_1:def 9
.= (((pr1 c2,c3,c4) + (pr1 c2,c3,c5)) * c2) + (((pr2 c2,c3,c4) + (pr2 c2,c3,c5)) * c3) by RLVECT_1:def 9 ;
hence ( pr1 c2,c3,(c4 + c5) = (pr1 c2,c3,c4) + (pr1 c2,c3,c5) & pr2 c2,c3,(c4 + c5) = (pr2 c2,c3,c4) + (pr2 c2,c3,c5) ) by E8, E6;
c4 - c5 = (((pr1 c2,c3,c4) - (pr1 c2,c3,c5)) * c2) + (((pr2 c2,c3,c4) - (pr2 c2,c3,c5)) * c3) by E9, E1;
hence ( pr1 c2,c3,(c4 - c5) = (pr1 c2,c3,c4) - (pr1 c2,c3,c5) & pr2 c2,c3,(c4 - c5) = (pr2 c2,c3,c4) - (pr2 c2,c3,c5) ) by E8, E6;
c6 * c4 = ((c6 * (pr1 c2,c3,c4)) * c2) + ((c6 * (pr2 c2,c3,c4)) * c3) by E9, E2;
hence ( pr1 c2,c3,(c6 * c4) = c6 * (pr1 c2,c3,c4) & pr2 c2,c3,(c6 * c4) = c6 * (pr2 c2,c3,c4) ) by E8, E6;
end;

definition
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
func Ortm a2,a3,a4 -> VECTOR of a1 equals :: ANALORT:def 1
((pr1 a2,a3,a4) * a2) + ((- (pr2 a2,a3,a4)) * a3);
correctness
coherence
((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3) is VECTOR of c1;
;
end;

:: deftheorem defines Ortm ANALORT:def 1 :
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds Ortm b2,b3,b4 = ((pr1 b2,b3,b4) * b2) + ((- (pr2 b2,b3,b4)) * b3);

theorem E8: :: ANALORT:1
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( Gen b2,b3 implies Ortm b2,b3,(b4 + b5) = (Ortm b2,b3,b4) + (Ortm b2,b3,b5) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E9: Gen c2,c3 ;
thus Ortm c2,c3,(c4 + c5) = ((pr1 c2,c3,(c4 + c5)) * c2) + ((- (pr2 c2,c3,(c4 + c5))) * c3)
.= (((pr1 c2,c3,c4) + (pr1 c2,c3,c5)) * c2) + ((- (pr2 c2,c3,(c4 + c5))) * c3) by E9, E7
.= (((pr1 c2,c3,c4) + (pr1 c2,c3,c5)) * c2) + ((- ((pr2 c2,c3,c4) + (pr2 c2,c3,c5))) * c3) by E9, E7
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + ((- ((pr2 c2,c3,c4) + (pr2 c2,c3,c5))) * c3) by RLVECT_1:def 9
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + (((pr2 c2,c3,c4) + (pr2 c2,c3,c5)) * (- c3)) by RLVECT_1:38
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + (- (((pr2 c2,c3,c4) + (pr2 c2,c3,c5)) * c3)) by RLVECT_1:39
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + (- (((pr2 c2,c3,c4) * c3) + ((pr2 c2,c3,c5) * c3))) by RLVECT_1:def 9
.= (((pr1 c2,c3,c4) * c2) + ((pr1 c2,c3,c5) * c2)) + ((- ((pr2 c2,c3,c4) * c3)) + (- ((pr2 c2,c3,c5) * c3))) by RLVECT_1:45
.= ((pr1 c2,c3,c4) * c2) + (((pr1 c2,c3,c5) * c2) + ((- ((pr2 c2,c3,c4) * c3)) + (- ((pr2 c2,c3,c5) * c3)))) by RLVECT_1:def 6
.= ((pr1 c2,c3,c4) * c2) + ((- ((pr2 c2,c3,c4) * c3)) + (((pr1 c2,c3,c5) * c2) + (- ((pr2 c2,c3,c5) * c3)))) by RLVECT_1:def 6
.= (((pr1 c2,c3,c4) * c2) + (- ((pr2 c2,c3,c4) * c3))) + (((pr1 c2,c3,c5) * c2) + (- ((pr2 c2,c3,c5) * c3))) by RLVECT_1:def 6
.= (((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * (- c3))) + (((pr1 c2,c3,c5) * c2) + (- ((pr2 c2,c3,c5) * c3))) by RLVECT_1:39
.= (((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * (- c3))) + (((pr1 c2,c3,c5) * c2) + ((pr2 c2,c3,c5) * (- c3))) by RLVECT_1:39
.= (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) + (((pr1 c2,c3,c5) * c2) + ((pr2 c2,c3,c5) * (- c3))) by RLVECT_1:38
.= (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) + (((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3)) by RLVECT_1:38
.= (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) + (Ortm c2,c3,c5)
.= (Ortm c2,c3,c4) + (Ortm c2,c3,c5) ;
end;

theorem E9: :: ANALORT:2
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1
for b5 being Real holds
( Gen b2,b3 implies Ortm b2,b3,(b5 * b4) = b5 * (Ortm b2,b3,b4) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
let c5 be Real;
assume E10: Gen c2,c3 ;
thus Ortm c2,c3,(c5 * c4) = ((pr1 c2,c3,(c5 * c4)) * c2) + ((- (pr2 c2,c3,(c5 * c4))) * c3)
.= ((c5 * (pr1 c2,c3,c4)) * c2) + ((- (pr2 c2,c3,(c5 * c4))) * c3) by E10, E7
.= ((c5 * (pr1 c2,c3,c4)) * c2) + ((- (c5 * (pr2 c2,c3,c4))) * c3) by E10, E7
.= ((c5 * (pr1 c2,c3,c4)) * c2) + ((c5 * (pr2 c2,c3,c4)) * (- c3)) by RLVECT_1:38
.= ((c5 * (pr1 c2,c3,c4)) * c2) + (- ((c5 * (pr2 c2,c3,c4)) * c3)) by RLVECT_1:39
.= ((c5 * (pr1 c2,c3,c4)) * c2) + (- (c5 * ((pr2 c2,c3,c4) * c3))) by RLVECT_1:def 9
.= ((c5 * (pr1 c2,c3,c4)) * c2) + (c5 * (- ((pr2 c2,c3,c4) * c3))) by RLVECT_1:39
.= (c5 * ((pr1 c2,c3,c4) * c2)) + (c5 * (- ((pr2 c2,c3,c4) * c3))) by RLVECT_1:def 9
.= c5 * (((pr1 c2,c3,c4) * c2) + (- ((pr2 c2,c3,c4) * c3))) by RLVECT_1:def 9
.= c5 * (((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * (- c3))) by RLVECT_1:39
.= c5 * (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) by RLVECT_1:38
.= c5 * (Ortm c2,c3,c4) ;
end;

theorem :: ANALORT:3
for b1 being RealLinearSpace
for b2, b3 being VECTOR of b1 holds
( Gen b2,b3 implies Ortm b2,b3,(0. b1) = 0. b1 )
proof
let c1 be RealLinearSpace;
let c2, c3 be VECTOR of c1;
assume E10: Gen c2,c3 ;
consider c4 being VECTOR of c1;
thus Ortm c2,c3,(0. c1) = Ortm c2,c3,(0 * c4) by RLVECT_1:23
.= 0 * (Ortm c2,c3,c4) by E10, E9
.= 0. c1 by RLVECT_1:23 ;
end;

theorem E10: :: ANALORT:4
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( Gen b2,b3 implies Ortm b2,b3,(- b4) = - (Ortm b2,b3,b4) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume E11: Gen c2,c3 ;
then E12: - c4 = - (((pr1 c2,c3,c4) * c2) + ((pr2 c2,c3,c4) * c3)) by E5
.= (- ((pr1 c2,c3,c4) * c2)) + (- ((pr2 c2,c3,c4) * c3)) by RLVECT_1:45
.= ((pr1 c2,c3,c4) * (- c2)) + (- ((pr2 c2,c3,c4) * c3)) by RLVECT_1:39
.= ((- (pr1 c2,c3,c4)) * c2) + (- ((pr2 c2,c3,c4) * c3)) by RLVECT_1:38
.= ((- (pr1 c2,c3,c4)) * c2) + ((pr2 c2,c3,c4) * (- c3)) by RLVECT_1:39
.= ((- (pr1 c2,c3,c4)) * c2) + ((- (pr2 c2,c3,c4)) * c3) by RLVECT_1:38 ;
thus Ortm c2,c3,(- c4) = ((pr1 c2,c3,(- c4)) * c2) + ((- (pr2 c2,c3,(- c4))) * c3)
.= ((- (pr1 c2,c3,c4)) * c2) + ((- (pr2 c2,c3,(- c4))) * c3) by E11, E12, E6
.= ((- (pr1 c2,c3,c4)) * c2) + ((- (- (pr2 c2,c3,c4))) * c3) by E11, E12, E6
.= ((pr1 c2,c3,c4) * (- c2)) + ((- (- (pr2 c2,c3,c4))) * c3) by RLVECT_1:38
.= (- ((pr1 c2,c3,c4) * c2)) + ((- (- (pr2 c2,c3,c4))) * c3) by RLVECT_1:39
.= (- ((pr1 c2,c3,c4) * c2)) + ((- (pr2 c2,c3,c4)) * (- c3)) by RLVECT_1:38
.= (- ((pr1 c2,c3,c4) * c2)) + (- ((- (pr2 c2,c3,c4)) * c3)) by RLVECT_1:39
.= - (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) by RLVECT_1:45
.= - (Ortm c2,c3,c4) ;
end;

theorem E11: :: ANALORT:5
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( Gen b2,b3 implies Ortm b2,b3,(b4 - b5) = (Ortm b2,b3,b4) - (Ortm b2,b3,b5) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E12: Gen c2,c3 ;
thus Ortm c2,c3,(c4 - c5) = Ortm c2,c3,(c4 + (- c5)) by RLVECT_1:def 11
.= (Ortm c2,c3,c4) + (Ortm c2,c3,(- c5)) by E12, E8
.= (Ortm c2,c3,c4) + (- (Ortm c2,c3,c5)) by E12, E10
.= (Ortm c2,c3,c4) - (Ortm c2,c3,c5) by RLVECT_1:def 11 ;
end;

theorem E12: :: ANALORT:6
for b1 being RealLinearSpace
for b2, b3, b4, b5 being VECTOR of b1 holds
( ( Gen b2,b3 & Ortm b2,b3,b4 = Ortm b2,b3,b5 ) implies ( b4 = b5 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be VECTOR of c1;
assume E13: ( Gen c2,c3 & Ortm c2,c3,c4 = Ortm c2,c3,c5 ) ;
then Ortm c2,c3,c4 = ((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3) ;
then (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) - (((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3)) = (((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3)) - (((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3)) ;
then (((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) - (((pr1 c2,c3,c5) * c2) + ((- (pr2 c2,c3,c5)) * c3)) = 0. c1 by RLVECT_1:28;
then ((((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) - ((pr1 c2,c3,c5) * c2)) - ((- (pr2 c2,c3,c5)) * c3) = 0. c1 by RLVECT_1:41;
then ((((pr1 c2,c3,c4) * c2) + ((- (pr2 c2,c3,c4)) * c3)) + (- ((pr1 c2,c3,c5) * c2))) - ((- (pr2 c2,c3,c5)) * c3) = 0. c1 by RLVECT_1:def 11;
then ((((pr1 c2,c3,c4) * c2) + (- ((pr1 c2,c3,c5) * c2))) + ((- (pr2 c2,c3,c4)) * c3)) - ((- (pr2 c2,c3,c5)) * c3) = 0. c1 by RLVECT_1:def 6;
then ((((pr1 c2,c3,c4) * c2) - ((pr1 c2,c3,c5) * c2)) + ((- (pr2 c2,c3,c4)) * c3)) - ((- (pr2 c2,c3,c5)) * c3) = 0. c1 by RLVECT_1:def 11;
then (((pr1 c2,c3,c4) * c2) - ((pr1 c2,c3,c5) * c2)) + (((- (pr2 c2,c3,c4)) * c3) - ((- (pr2 c2,c3,c5)) * c3)) = 0. c1 by RLVECT_1:42;
then (((pr1 c2,c3,c4) - (pr1 c2,c3,c5)) * c2) + (((- (pr2 c2,c3,c4)) * c3) - ((- (pr2 c2,c3,c5)) * c3)) = 0. c1 by RLVECT_1:49;
then (((pr1 c2,c3,c4) - (pr1 c2,c3,c5)) * c2) + (((- (pr2 c2,c3,c4)) - (- (pr2 c2,c3,c5))) * c3) = 0. c1 by RLVECT_1:49;
then ( (pr1 c2,c3,c4) - (pr1 c2,c3,c5) = 0 & (- (pr2 c2,c3,c4)) - (- (pr2 c2,c3,c5)) = 0 ) by E13, ANALMETR:def 1;
then E14: ( pr1 c2,c3,c4 = pr1 c2,c3,c5 & - (pr2 c2,c3,c4) = - (pr2 c2,c3,c5) ) ;
hence c4 = ((pr1 c2,c3,c5) * c2) + ((pr2 c2,c3,c4) * c3) by E13, E5
.= ((pr1 c2,c3,c5) * c2) + ((pr2 c2,c3,c5) * c3) by E14
.= c5 by E13, E5 ;

end;

theorem E13: :: ANALORT:7
for b1 being RealLinearSpace
for b2, b3, b4 being VECTOR of b1 holds
( Gen b2,b3 implies Ortm b2,b3,(Ortm b2,b3,b4) = b4 )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be VECTOR of c1;
assume E14: Gen c2,c3 ;
thus Ortm c2,c3