:: ANPROJ_2 semantic presentation

theorem Th1: :: ANPROJ_2:1
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( ( for b5, b6, b7 being Real holds
( ((b5 * b2) + (b6 * b3)) + (b7 * b4) = 0. b1 implies ( b5 = 0 & b6 = 0 & b7 = 0 ) ) ) implies ( b2 is_Prop_Vect & b3 is_Prop_Vect & b4 is_Prop_Vect & not b2,b3,b4 are_LinDep & not are_Prop b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume E2: for b1, b2, b3 being Real holds
( ((b1 * c2) + (b2 * c3)) + (b3 * c4) = 0. c1 implies ( b1 = 0 & b2 = 0 & b3 = 0 ) ) ;
thus ( c2 is_Prop_Vect & c3 is_Prop_Vect & c4 is_Prop_Vect )
proof
E3: now
assume not c2 is_Prop_Vect ;
then E4: c2 = 0. c1 by RLVECT_1:def 13;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= ((0. c1) + (0. c1)) + (0. c1) by RLVECT_1:10
.= ((1 * c2) + (0. c1)) + (0. c1) by E4, RLVECT_1:def 9
.= ((1 * c2) + (0 * c3)) + (0. c1) by RLVECT_1:23
.= ((1 * c2) + (0 * c3)) + (0 * c4) by RLVECT_1:23 ;
hence not verum by E2;
end;
E4: now
assume not c3 is_Prop_Vect ;
then E5: c3 = 0. c1 by RLVECT_1:def 13;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= ((0. c1) + (0. c1)) + (0. c1) by RLVECT_1:10
.= ((0. c1) + (1 * c3)) + (0. c1) by E5, RLVECT_1:def 9
.= ((0 * c2) + (1 * c3)) + (0. c1) by RLVECT_1:23
.= ((0 * c2) + (1 * c3)) + (0 * c4) by RLVECT_1:23 ;
hence not verum by E2;
end;
now
assume not c4 is_Prop_Vect ;
then E5: c4 = 0. c1 by RLVECT_1:def 13;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= ((0. c1) + (0. c1)) + (0. c1) by RLVECT_1:10
.= ((0. c1) + (0. c1)) + (1 * c4) by E5, RLVECT_1:def 9
.= ((0 * c2) + (0. c1)) + (1 * c4) by RLVECT_1:23
.= ((0 * c2) + (0 * c3)) + (1 * c4) by RLVECT_1:23 ;
hence not verum by E2;
end;
hence ( c2 is_Prop_Vect & c3 is_Prop_Vect & c4 is_Prop_Vect ) by E3, E4;
end;
thus not c2,c3,c4 are_LinDep by E2, ANPROJ_1:def 3;
hence not are_Prop c2,c3 by ANPROJ_1:17;
end;

Lemma2: for b1 being RealLinearSpace
for b2, b3 being Element of b1 holds
( ( for b4, b5 being Real holds
( (b4 * b2) + (b5 * b3) = 0. b1 implies ( b4 = 0 & b5 = 0 ) ) ) implies ( b2 is_Prop_Vect & b3 is_Prop_Vect & not are_Prop b2,b3 ) )
proof
let c1 be RealLinearSpace;
let c2, c3 be Element of c1;
assume E3: for b1, b2 being Real holds
( (b1 * c2) + (b2 * c3) = 0. c1 implies ( b1 = 0 & b2 = 0 ) ) ;
thus ( c2 is_Prop_Vect & c3 is_Prop_Vect )
proof
E4: now
assume not c2 is_Prop_Vect ;
then E5: c2 = 0. c1 by RLVECT_1:def 13;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= (1 * c2) + (0. c1) by E5, RLVECT_1:def 9
.= (1 * c2) + (0 * c3) by RLVECT_1:23 ;
hence not verum by E3;
end;
now
assume not c3 is_Prop_Vect ;
then E5: c3 = 0. c1 by RLVECT_1:def 13;
0. c1 = (0. c1) + (0. c1) by RLVECT_1:10
.= (0. c1) + (1 * c3) by E5, RLVECT_1:def 9
.= (0 * c2) + (1 * c3) by RLVECT_1:23 ;
hence not verum by E3;
end;
hence ( c2 is_Prop_Vect & c3 is_Prop_Vect ) by E4;
end;
given c4, c5 being Real such that E4: c4 * c2 = c5 * c3 and
E5: ( c4 <> 0 & c5 <> 0 ) ; :: according to ANPROJ_1:def 2
0. c1 = (c4 * c2) - (c5 * c3) by E4, RLVECT_1:28
.= (c4 * c2) + (- (c5 * c3)) by RLVECT_1:def 11
.= (c4 * c2) + (c5 * (- c3)) by RLVECT_1:39
.= (c4 * c2) + ((- c5) * c3) by RLVECT_1:38 ;
hence not verum by E3, E5;
end;

theorem Th2: :: ANPROJ_2:2
for b1 being RealLinearSpace
for b2, b3, b4, b5 being Element of b1 holds
( ( for b6, b7, b8, b9 being Real holds
( (((b6 * b2) + (b7 * b3)) + (b8 * b4)) + (b9 * b5) = 0. b1 implies ( b6 = 0 & b7 = 0 & b8 = 0 & b9 = 0 ) ) ) implies ( b2 is_Prop_Vect & b3 is_Prop_Vect & not are_Prop b2,b3 & b4 is_Prop_Vect & b5 is_Prop_Vect & not are_Prop b4,b5 & not b2,b3,b4 are_LinDep & not b4,b5,b2 are_LinDep ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be Element of c1;
assume E4: for b1, b2, b3, b4 being Real holds
( (((b1 * c2) + (b2 * c3)) + (b3 * c4)) + (b4 * c5) = 0. c1 implies ( b1 = 0 & b2 = 0 & b3 = 0 & b4 = 0 ) ) ;
E5: now
let c6, c7, c8 be Real;
assume ((c6 * c4) + (c7 * c5)) + (c8 * c2) = 0. c1 ;
then 0. c1 = ((c8 * c2) + (c6 * c4)) + (c7 * c5) by RLVECT_1:def 6
.= (((c8 * c2) + (0. c1)) + (c6 * c4)) + (c7 * c5) by RLVECT_1:10
.= (((c8 * c2) + (0 * c3)) + (c6 * c4)) + (c7 * c5) by RLVECT_1:23 ;
hence ( c6 = 0 & c7 = 0 & c8 = 0 ) by E4;
end;
now
let c6, c7, c8 be Real;
assume ((c6 * c2) + (c7 * c3)) + (c8 * c4) = 0. c1 ;
then 0. c1 = (((c6 * c2) + (c7 * c3)) + (c8 * c4)) + (0. c1) by RLVECT_1:10
.= (((c6 * c2) + (c7 * c3)) + (c8 * c4)) + (0 * c5) by RLVECT_1:23 ;
hence ( c6 = 0 & c7 = 0 & c8 = 0 ) by E4;
end;
hence ( c2 is_Prop_Vect & c3 is_Prop_Vect & not are_Prop c2,c3 & c4 is_Prop_Vect & c5 is_Prop_Vect & not are_Prop c4,c5 & not c2,c3,c4 are_LinDep & not c4,c5,c2 are_LinDep ) by E5, Th1;
end;

Lemma4: for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1
for b5, b6, b7, b8 being Real holds b5 * (((b6 * b2) + (b7 * b3)) + (b8 * b4)) = (((b5 * b6) * b2) + ((b5 * b7) * b3)) + ((b5 * b8) * b4)
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
let c5, c6, c7, c8 be Real;
thus (((c5 * c6) * c2) + ((c5 * c7) * c3)) + ((c5 * c8) * c4) = ((c5 * (c6 * c2)) + ((c5 * c7) * c3)) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= ((c5 * (c6 * c2)) + (c5 * (c7 * c3))) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= (c5 * ((c6 * c2) + (c7 * c3))) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= (c5 * ((c6 * c2) + (c7 * c3))) + (c5 * (c8 * c4)) by RLVECT_1:def 9
.= c5 * (((c6 * c2) + (c7 * c3)) + (c8 * c4)) by RLVECT_1:def 9 ;
end;

Lemma5: for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7 being Element of b1 holds ((b2 + b3) + b4) + ((b5 + b6) + b7) = ((b2 + b5) + (b3 + b6)) + (b4 + b7)
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6, c7 be Element of c1;
thus ((c2 + c5) + (c3 + c6)) + (c4 + c7) = (c5 + (c2 + (c3 + c6))) + (c4 + c7) by RLVECT_1:def 6
.= (c5 + ((c2 + c3) + c6)) + (c4 + c7) by RLVECT_1:def 6
.= ((c5 + c6) + (c2 + c3)) + (c4 + c7) by RLVECT_1:def 6
.= (c5 + c6) + ((c2 + c3) + (c4 + c7)) by RLVECT_1:def 6
.= (c5 + c6) + (((c2 + c3) + c4) + c7) by RLVECT_1:def 6
.= ((c2 + c3) + c4) + ((c5 + c6) + c7) by RLVECT_1:def 6 ;
end;

theorem Th3: :: ANPROJ_2:3
for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1 holds
( ( for b5 being Element of b1 holds
ex b6, b7, b8 being Real st b5 = ((b6 * b2) + (b7 * b3)) + (b8 * b4) ) & ( for b5, b6, b7 being Real holds
( ((b5 * b2) + (b6 * b3)) + (b7 * b4) = 0. b1 implies ( b5 = 0 & b6 = 0 & b7 = 0 ) ) ) implies for b5, b6 being Element of b1 holds
ex b7 being Element of b1 st
( b2,b3,b7 are_LinDep & b5,b6,b7 are_LinDep & b7 is_Prop_Vect ) )
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
assume that
E7: for b1 being Element of c1 holds
ex b2, b3, b4 being Real st b1 = ((b2 * c2) + (b3 * c3)) + (b4 * c4) and
E8: for b1, b2, b3 being Real holds
( ((b1 * c2) + (b2 * c3)) + (b3 * c4) = 0. c1 implies ( b1 = 0 & b2 = 0 & b3 = 0 ) ) ;
let c5, c6 be Element of c1;
consider c7, c8, c9 being Real such that
E9: c5 = ((c7 * c2) + (c8 * c3)) + (c9 * c4) by E7;
consider c10, c11, c12 being Real such that
E10: c6 = ((c10 * c2) + (c11 * c3)) + (c12 * c4) by E7;
E11: ( c2 is_Prop_Vect & c3 is_Prop_Vect & c4 is_Prop_Vect & not c2,c3,c4 are_LinDep & not are_Prop c2,c3 ) by E8, Th1;
E12: for b1, b2 being Real holds (b1 * c5) + (b2 * c6) = ((((b1 * c7) + (b2 * c10)) * c2) + (((b1 * c8) + (b2 * c11)) * c3)) + (((b1 * c9) + (b2 * c12)) * c4)
proof
let c13, c14 be Real;
c13 * c5 = (((c13 * c7) * c2) + ((c13 * c8) * c3)) + ((c13 * c9) * c4) by E9, Lemma4;
hence (c13 * c5) + (c14 * c6) = ((((c13 * c7) * c2) + ((c13 * c8) * c3)) + ((c13 * c9) * c4)) + ((((c14 * c10) * c2) + ((c14 * c11) * c3)) + ((c14 * c12) * c4)) by E10, Lemma4
.= ((((c13 * c7) * c2) + ((c14 * c10) * c2)) + (((c13 * c8) * c3) + ((c14 * c11) * c3))) + (((c13 * c9) * c4) + ((c14 * c12) * c4)) by Lemma5
.= ((((c13 * c7) + (c14 * c10)) * c2) + (((c13 * c8) * c3) + ((c14 * c11) * c3))) + (((c13 * c9) * c4) + ((c14 * c12) * c4)) by RLVECT_1:def 9
.= ((((c13 * c7) + (c14 * c10)) * c2) + (((c13 * c8) + (c14 * c11)) * c3)) + (((c13 * c9) * c4) + ((c14 * c12) * c4)) by RLVECT_1:def 9
.= ((((c13 * c7) + (c14 * c10)) * c2) + (((c13 * c8) + (c14 * c11)) * c3)) + (((c13 * c9) + (c14 * c12)) * c4) by RLVECT_1:def 9 ;

end;
E13: now
assume E14: not ( not are_Prop c5,c6 & c5 is_Prop_Vect & c6 is_Prop_Vect ) ;
E15: now
assume E16: are_Prop c5,c6 ;
E17: c2,c3,c3 are_LinDep by ANPROJ_1:16;
c5,c6,c3 are_LinDep by E16, ANPROJ_1:16;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E11, E17;
end;
E16: now
assume not c5 is_Prop_Vect ;
then E17: c5 = 0. c1 by RLVECT_1:def 13;
E18: c2,c3,c3 are_LinDep by ANPROJ_1:16;
c5,c6,c3 are_LinDep by E17, ANPROJ_1:15;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E11, E18;
end;
now
assume not c6 is_Prop_Vect ;
then E17: c6 = 0. c1 by RLVECT_1:def 13;
E18: c2,c3,c3 are_LinDep by ANPROJ_1:16;
c5,c6,c3 are_LinDep by E17, ANPROJ_1:15;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E11, E18;
end;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E14, E15, E16;
end;
E14: now
assume E15: ( not are_Prop c5,c6 & c5 is_Prop_Vect & c6 is_Prop_Vect & c9 = 0 ) ;
now
set c13 = 1;
set c14 = 0;
set c15 = (1 * c5) + (0 * c6);
E16: (1 * c5) + (0 * c6) is_Prop_Vect
proof
(1 * c5) + (0 * c6) = c5 + (0 * c6) by RLVECT_1:def 9
.= c5 + (0. c1) by RLVECT_1:23
.= c5 by RLVECT_1:10 ;
hence (1 * c5) + (0 * c6) is_Prop_Vect by E15;
end;
(1 * c9) + (0 * c12) = 0 by E15;
then (1 * c5) + (0 * c6) = ((((1 * c7) + (0 * c10)) * c2) + (((1 * c8) + (0 * c11)) * c3)) + (0 * c4) by E12
.= ((((1 * c7) + (0 * c10)) * c2) + (((1 * c8) + (0 * c11)) * c3)) + (0. c1) by RLVECT_1:23
.= (((1 * c7) + (0 * c10)) * c2) + (((1 * c8) + (0 * c11)) * c3) by RLVECT_1:10 ;
then E17: c2,c3,(1 * c5) + (0 * c6) are_LinDep by E11, ANPROJ_1:11;
c5,c6,(1 * c5) + (0 * c6) are_LinDep by E15, ANPROJ_1:11;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E16, E17;
end;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) ;
end;
now
assume E15: ( not are_Prop c5,c6 & c5 is_Prop_Vect & c6 is_Prop_Vect & c9 <> 0 ) ;
E16: now
assume E17: c12 = 0 ;
set c13 = 0;
set c14 = 1;
set c15 = (0 * c5) + (1 * c6);
E18: (0 * c5) + (1 * c6) is_Prop_Vect
proof
(0 * c5) + (1 * c6) = (0 * c5) + c6 by RLVECT_1:def 9
.= (0. c1) + c6 by RLVECT_1:23
.= c6 by RLVECT_1:10 ;
hence (0 * c5) + (1 * c6) is_Prop_Vect by E15;
end;
(0 * c9) + (1 * c12) = 0 by E17;
then (0 * c5) + (1 * c6) = ((((0 * c7) + (1 * c10)) * c2) + (((0 * c8) + (1 * c11)) * c3)) + (0 * c4) by E12
.= ((((0 * c7) + (1 * c10)) * c2) + (((0 * c8) + (1 * c11)) * c3)) + (0. c1) by RLVECT_1:23
.= (((0 * c7) + (1 * c10)) * c2) + (((0 * c8) + (1 * c11)) * c3) by RLVECT_1:10 ;
then E19: c2,c3,(0 * c5) + (1 * c6) are_LinDep by E11, ANPROJ_1:11;
c5,c6,(0 * c5) + (1 * c6) are_LinDep by E15, ANPROJ_1:11;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E18, E19;
end;
now
assume E17: c12 <> 0 ;
set c13 = 1;
set c14 = - (c9 * (c12 " ));
set c15 = (1 * c5) + ((- (c9 * (c12 " ))) * c6);
c12 " <> 0 by E17, XCMPLX_1:203;
then E18: c9 * (c12 " ) <> 0 by E15, XCMPLX_1:6;
E19: (1 * c5) + ((- (c9 * (c12 " ))) * c6) is_Prop_Vect
proof
assume not (1 * c5) + ((- (c9 * (c12 " ))) * c6) is_Prop_Vect ;
then 0. c1 = (1 * c5) + ((- (c9 * (c12 " ))) * c6) by RLVECT_1:def 13
.= (1 * c5) + ((c9 * (c12 " )) * (- c6)) by RLVECT_1:38
.= (1 * c5) + (- ((c9 * (c12 " )) * c6)) by RLVECT_1:39 ;
then - (1 * c5) = - ((c9 * (c12 " )) * c6) by RLVECT_1:def 10;
then 1 * c5 = (c9 * (c12 " )) * c6 by RLVECT_1:31;
hence not verum by E15, E18, ANPROJ_1:def 2;
end;
(1 * c9) + ((- (c9 * (c12 " ))) * c12) = c9 + ((- c9) * ((c12 " ) * c12))
.= c9 + ((- c9) * 1) by E17, XCMPLX_0:def 7
.= 0 ;
then (1 * c5) + ((- (c9 * (c12 " ))) * c6) = ((((1 * c7) + ((- (c9 * (c12 " ))) * c10)) * c2) + (((1 * c8) + ((- (c9 * (c12 " ))) * c11)) * c3)) + (0 * c4) by E12
.= ((((1 * c7) + ((- (c9 * (c12 " ))) * c10)) * c2) + (((1 * c8) + ((- (c9 * (c12 " ))) * c11)) * c3)) + (0. c1) by RLVECT_1:23
.= (((1 * c7) + ((- (c9 * (c12 " ))) * c10)) * c2) + (((1 * c8) + ((- (c9 * (c12 " ))) * c11)) * c3) by RLVECT_1:10 ;
then E20: c2,c3,(1 * c5) + ((- (c9 * (c12 " ))) * c6) are_LinDep by E11, ANPROJ_1:11;
c5,c6,(1 * c5) + ((- (c9 * (c12 " ))) * c6) are_LinDep by E15, ANPROJ_1:11;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E19, E20;
end;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E16;
end;
hence ex b1 being Element of c1 st
( c2,c3,b1 are_LinDep & c5,c6,b1 are_LinDep & b1 is_Prop_Vect ) by E13, E14;
end;

Lemma7: for b1 being RealLinearSpace
for b2, b3, b4, b5 being Element of b1
for b6, b7, b8, b9, b10 being Real holds b6 * ((((b7 * b2) + (b8 * b3)) + (b9 * b4)) + (b10 * b5)) = ((((b6 * b7) * b2) + ((b6 * b8) * b3)) + ((b6 * b9) * b4)) + ((b6 * b10) * b5)
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5 be Element of c1;
let c6, c7, c8, c9, c10 be Real;
thus ((((c6 * c7) * c2) + ((c6 * c8) * c3)) + ((c6 * c9) * c4)) + ((c6 * c10) * c5) = (((c6 * (c7 * c2)) + ((c6 * c8) * c3)) + ((c6 * c9) * c4)) + ((c6 * c10) * c5) by RLVECT_1:def 9
.= (((c6 * (c7 * c2)) + (c6 * (c8 * c3))) + ((c6 * c9) * c4)) + ((c6 * c10) * c5) by RLVECT_1:def 9
.= ((c6 * ((c7 * c2) + (c8 * c3))) + ((c6 * c9) * c4)) + ((c6 * c10) * c5) by RLVECT_1:def 9
.= ((c6 * ((c7 * c2) + (c8 * c3))) + (c6 * (c9 * c4))) + ((c6 * c10) * c5) by RLVECT_1:def 9
.= ((c6 * ((c7 * c2) + (c8 * c3))) + (c6 * (c9 * c4))) + (c6 * (c10 * c5)) by RLVECT_1:def 9
.= (c6 * (((c7 * c2) + (c8 * c3)) + (c9 * c4))) + (c6 * (c10 * c5)) by RLVECT_1:def 9
.= c6 * ((((c7 * c2) + (c8 * c3)) + (c9 * c4)) + (c10 * c5)) by RLVECT_1:def 9 ;
end;

Lemma8: for b1 being RealLinearSpace
for b2, b3, b4, b5, b6, b7, b8, b9 being Element of b1 holds (((b2 + b3) + b4) + b5) + (((b6 + b7) + b8) + b9) = (((b2 + b6) + (b3 + b7)) + (b4 + b8)) + (b5 + b9)
proof
let c1 be RealLinearSpace;
let c2, c3, c4, c5, c6, c7, c8, c9 be Element of c1;
thus (((c2 + c6) + (c3 + c7)) + (c4 + c8)) + (c5 + c9) = ((c6 + (c2 + (c3 + c7))) + (c4 + c8)) + (c5 + c9) by RLVECT_1:def 6
.= ((c6 + ((c2 + c3) + c7)) + (c4 + c8)) + (c5 + c9) by RLVECT_1:def 6
.= (((c6 + c7) + (c2 + c3)) + (c4 + c8)) + (c5 + c9) by RLVECT_1:def 6
.= ((c6 + c7) + ((c2 + c3) + (c4 + c8))) + (c5 + c9) by RLVECT_1:def 6
.= ((c6 + c7) + (((c2 + c3) + c4) + c8)) + (c5 + c9) by RLVECT_1:def 6
.= (((c6 + c7) + c8) + ((c2 + c3) + c4)) + (c5 + c9) by RLVECT_1:def 6
.= ((c2 + c3) + c4) + (((c6 + c7) + c8) + (c5 + c9)) by RLVECT_1:def 6
.= ((c2 + c3) + c4) + (c5 + (c9 + ((c6 + c7) + c8))) by RLVECT_1:def 6
.= (((c2 + c3) + c4) + c5) + (((c6 + c7) + c8) + c9) by RLVECT_1:def 6 ;
end;

Lemma9: for b1 being RealLinearSpace
for b2, b3, b4 being Element of b1
for b5, b6, b7, b8 being Real holds b5 * (((b6 * b2) + (b7 * b3)) + (b8 * b4)) = (((b5 * b6) * b2) + ((b5 * b7) * b3)) + ((b5 * b8) * b4)
proof
let c1 be RealLinearSpace;
let c2, c3, c4 be Element of c1;
let c5, c6, c7, c8 be Real;
thus (((c5 * c6) * c2) + ((c5 * c7) * c3)) + ((c5 * c8) * c4) = ((c5 * (c6 * c2)) + ((c5 * c7) * c3)) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= ((c5 * (c6 * c2)) + (c5 * (c7 * c3))) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= (c5 * ((c6 * c2) + (c7 * c3))) + ((c5 * c8) * c4) by RLVECT_1:def 9
.= (c5 * ((c6 * c2) + (c7 * c3))) + (c5 * (c8 * c4)) by RLVECT_1:def 9
.= c5 * (((c6 * c2) + (c7 * c3)) + (c8 * c4)) by