let V be RealLinearSpace; :: thesis: for v1, v2, w1, w2 being VECTOR of V st v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} holds
( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
let v1, v2, w1, w2 be VECTOR of V; :: thesis: ( v1 <> v2 & {v1,v2} is linearly-independent & v1 in Lin {w1,w2} & v2 in Lin {w1,w2} implies ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 ) )
assume that
A1: v1 <> v2 and
A2: {v1,v2} is linearly-independent and
A3: v1 in Lin {w1,w2} and
A4: v2 in Lin {w1,w2} ; :: thesis: ( Lin {w1,w2} = Lin {v1,v2} & {w1,w2} is linearly-independent & w1 <> w2 )
consider r1, r2 being Real such that
A5: v1 = (r1 * w1) + (r2 * w2) by A3, Th14;
consider r3, r4 being Real such that
A6: v2 = (r3 * w1) + (r4 * w2) by A4, Th14;
set t = (r1 * r4) - (r2 * r3);

A7: now

assume ( r1 = 0 & r2 = 0 ) ; :: thesis: contradiction
then v1 = (0. V) + (0 * w2) by A5, RLVECT_1:23
.= (0. V) + (0. V) by RLVECT_1:23
.= 0. V by RLVECT_1:10 ;
hence contradiction by A2, RLVECT_3:12; :: thesis: verum

end;

now

assume A8: r1 * r4 = r2 * r3 ; :: thesis: contradiction

now

per cases ( r1 <> 0 or r2 <> 0 ) by A7;

suppose A9: r1 <> 0 ; :: thesis: contradiction

((r1 " ) * r1) * r4 = (r1 " ) * (r2 * r3) by A8, XCMPLX_1:4;
then 1 * r4 = (r1 " ) * (r2 * r3) by A9, XCMPLX_0:def 7;
then v2 = (r3 * w1) + ((r3 * ((r1 " ) * r2)) * w2) by A6
.= (r3 * w1) + (r3 * (((r1 " ) * r2) * w2)) by RLVECT_1:def 10
.= (r3 * 1) * (w1 + (((r1 " ) * r2) * w2)) by RLVECT_1:def 8
.= (r3 * ((r1 " ) * r1)) * (w1 + (((r1 " ) * r2) * w2)) by A9, XCMPLX_0:def 7
.= ((r3 * (r1 " )) * r1) * (w1 + (((r1 " ) * r2) * w2))
.= (r3 * (r1 " )) * (r1 * (w1 + (((r1 " ) * r2) * w2))) by RLVECT_1:def 10
.= (r3 * (r1 " )) * ((r1 * w1) + (r1 * (((r1 " ) * r2) * w2))) by RLVECT_1:def 8
.= (r3 * (r1 " )) * ((r1 * w1) + ((r1 * ((r1 " ) * r2)) * w2)) by RLVECT_1:def 10
.= (r3 * (r1 " )) * ((r1 * w1) + (((r1 * (r1 " )) * r2) * w2))
.= (r3 * (r1 " )) * ((r1 * w1) + ((1 * r2) * w2)) by A9, XCMPLX_0:def 7
.= (r3 * (r1 " )) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:13; :: thesis: verum

end;

suppose A10: r2 <> 0 ; :: thesis: contradiction

(r2 " ) * (r1 * r4) = (r2 " ) * (r2 * r3) by A8
.= ((r2 " ) * r2) * r3
.= 1 * r3 by A10, XCMPLX_0:def 7
.= r3 ;
then v2 = ((r4 * ((r2 " ) * r1)) * w1) + (r4 * w2) by A6
.= (r4 * (((r2 " ) * r1) * w1)) + (r4 * w2) by RLVECT_1:def 10
.= (r4 * 1) * ((((r2 " ) * r1) * w1) + w2) by RLVECT_1:def 8
.= (r4 * ((r2 " ) * r2)) * ((((r2 " ) * r1) * w1) + w2) by A10, XCMPLX_0:def 7
.= ((r4 * (r2 " )) * r2) * ((((r2 " ) * r1) * w1) + w2)
.= (r4 * (r2 " )) * (r2 * ((((r2 " ) * r1) * w1) + w2)) by RLVECT_1:def 10
.= (r4 * (r2 " )) * ((r2 * (((r2 " ) * r1) * w1)) + (r2 * w2)) by RLVECT_1:def 8
.= (r4 * (r2 " )) * (((r2 * ((r2 " ) * r1)) * w1) + (r2 * w2)) by RLVECT_1:def 10
.= (r4 * (r2 " )) * ((((r2 * (r2 " )) * r1) * w1) + (r2 * w2))
.= (r4 * (r2 " )) * (((1 * r1) * w1) + (r2 * w2)) by A10, XCMPLX_0:def 7
.= (r4 * (r2 " )) * ((r1 * w1) + (r2 * w2)) ;
hence contradiction by A1, A2, A5, RLVECT_3:13; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then A11: (r1 * r4) - (r2 * r3) <> 0 ;

A12: now

assume A13: r2 <> 0 ; :: thesis: ( w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2)) & w2 = (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) )
(r2 " ) * v1 = ((r2 " ) * (r1 * w1)) + ((r2 " ) * (r2 * w2)) by A5, RLVECT_1:def 8
.= (((r2 " ) * r1) * w1) + ((r2 " ) * (r2 * w2)) by RLVECT_1:def 10
.= (((r2 " ) * r1) * w1) + (((r2 " ) * r2) * w2) by RLVECT_1:def 10
.= (((r2 " ) * r1) * w1) + (1 * w2) by A13, XCMPLX_0:def 7
.= (((r2 " ) * r1) * w1) + w2 by RLVECT_1:def 11 ;
then A14: w2 = ((r2 " ) * v1) - (((r2 " ) * r1) * w1) by RLSUB_2:78;
then w2 = ((r2 " ) * v1) - ((r2 " ) * (r1 * w1)) by RLVECT_1:def 10;
then v2 = (r3 * w1) + (r4 * ((r2 " ) * (v1 - (r1 * w1)))) by A6, RLVECT_1:48
.= (r3 * w1) + ((r4 * (r2 " )) * (v1 - (r1 * w1))) by RLVECT_1:def 10
.= (r3 * w1) + (((r4 * (r2 " )) * v1) - ((r4 * (r2 " )) * (r1 * w1))) by RLVECT_1:48
.= ((r3 * w1) + ((r4 * (r2 " )) * v1)) - ((r4 * (r2 " )) * (r1 * w1)) by RLVECT_1:def 6
.= (((r4 * (r2 " )) * v1) + (r3 * w1)) - (((r4 * (r2 " )) * r1) * w1) by RLVECT_1:def 10
.= ((r4 * (r2 " )) * v1) + ((r3 * w1) - (((r4 * (r2 " )) * r1) * w1)) by RLVECT_1:def 6
.= ((r4 * (r2 " )) * v1) + ((r3 - ((r4 * (r2 " )) * r1)) * w1) by RLVECT_1:49 ;
then r2 * v2 = (r2 * ((r4 * (r2 " )) * v1)) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1)) by RLVECT_1:def 8
.= ((r2 * (r4 * (r2 " ))) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1)) by RLVECT_1:def 10
.= ((r4 * (r2 * (r2 " ))) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1))
.= ((r4 * 1) * v1) + (r2 * ((r3 - ((r4 * (r2 " )) * r1)) * w1)) by A13, XCMPLX_0:def 7
.= (r4 * v1) + ((r2 * (r3 - ((r4 * (r2 " )) * r1))) * w1) by RLVECT_1:def 10
.= (r4 * v1) + (((r2 * r3) - ((r2 * (r2 " )) * (r4 * r1))) * w1)
.= (r4 * v1) + (((r2 * r3) - (1 * (r4 * r1))) * w1) by A13, XCMPLX_0:def 7
.= (r4 * v1) + ((- ((r1 * r4) - (r2 * r3))) * w1)
.= (r4 * v1) + (- (((r1 * r4) - (r2 * r3)) * w1)) by Th6 ;
then - (((r1 * r4) - (r2 * r3)) * w1) = (r2 * v2) - (r4 * v1) by RLSUB_2:78;
then ((r1 * r4) - (r2 * r3)) * w1 = - ((r2 * v2) - (r4 * v1)) by RLVECT_1:30
.= (r4 * v1) + (- (r2 * v2)) by RLVECT_1:47 ;
then ((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) * w1 = (((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def 10;
then 1 * w1 = (((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) + (- (r2 * v2))) by A11, XCMPLX_0:def 7;
then w1 = (((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) + (- (r2 * v2))) by RLVECT_1:def 11
.= ((((r1 * r4) - (r2 * r3)) " ) * (r4 * v1)) + ((((r1 * r4) - (r2 * r3)) " ) * (- (r2 * v2))) by RLVECT_1:def 8
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((((r1 * r4) - (r2 * r3)) " ) * (- (r2 * v2))) by RLVECT_1:def 10
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((((r1 * r4) - (r2 * r3)) " ) * ((- r2) * v2)) by Th6
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * (- r2)) * v2) by RLVECT_1:def 10
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (((- (((r1 * r4) - (r2 * r3)) " )) * r2) * v2)
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((- (((r1 * r4) - (r2 * r3)) " )) * (r2 * v2)) by RLVECT_1:def 10
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- ((((r1 * r4) - (r2 * r3)) " ) * (r2 * v2))) by Th6 ;
hence w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2)) by RLVECT_1:def 10; :: thesis: w2 = (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2)
then A15: w2 = ((r2 " ) * v1) - (((r2 " ) * r1) * (((((r1 * r4) - (r2 * r3)) " ) * (r4 * v1)) - (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2))) by A14, RLVECT_1:def 10
.= ((r2 " ) * v1) - (((r2 " ) * r1) * (((((r1 * r4) - (r2 * r3)) " ) * (r4 * v1)) - ((((r1 * r4) - (r2 * r3)) " ) * (r2 * v2)))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - (((r2 " ) * r1) * ((((r1 * r4) - (r2 * r3)) " ) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:48
.= ((r2 " ) * v1) - (((r1 * (r2 " )) * (((r1 * r4) - (r2 * r3)) " )) * ((r4 * v1) - (r2 * v2))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) " ) * (r2 " ))) * ((r4 * v1) - (r2 * v2)))
.= ((r2 " ) * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) " ) * (r2 " )) * ((r4 * v1) - (r2 * v2)))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((r2 " ) * ((r4 * v1) - (r2 * v2))))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * (r4 * v1)) - ((r2 " ) * (r2 * v2))))) by RLVECT_1:48
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * (r4 * v1)) - (((r2 " ) * r2) * v2)))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((((r2 " ) * r4) * v1) - (((r2 " ) * r2) * v2)))) by RLVECT_1:def 10
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((((r2 " ) * r4) * v1) - (1 * v2)))) by A13, XCMPLX_0:def 7
.= ((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * ((((r2 " ) * r4) * v1) - v2))) by RLVECT_1:def 11
.= ((r2 " ) * v1) - (r1 * (((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)) - ((((r1 * r4) - (r2 * r3)) " ) * v2))) by RLVECT_1:48
.= ((r2 " ) * v1) - ((r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1))) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * v2))) by RLVECT_1:48
.= (((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)))) + (r1 * ((((r1 * r4) - (r2 * r3)) " ) * v2)) by RLVECT_1:43
.= (((r2 " ) * v1) - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * (((r2 " ) * r4) * v1)))) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2) by RLVECT_1:def 10
.= (((r2 " ) * v1) - ((r1 * (((r1 * r4) - (r2 * r3)) " )) * (((r2 " ) * r4) * v1))) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2) by RLVECT_1:def 10
.= (((r2 " ) * v1) - (((r1 * (((r1 * r4) - (r2 * r3)) " )) * ((r2 " ) * r4)) * v1)) + ((r1 * (((r1 * r4) - (r2 * r3)) " )) * v2) by RLVECT_1:def 10
.= (((r2 " ) - ((r1 * (((r1 * r4) - (r2 * r3)) " )) * ((r2 " ) * r4))) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) by RLVECT_1:49 ;
(r2 " ) - ((r1 * (((r1 * r4) - (r2 * r3)) " )) * ((r2 " ) * r4)) = (r2 " ) * (1 - (r1 * ((((r1 * r4) - (r2 * r3)) " ) * r4)))
.= (r2 " ) * (((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) - ((((r1 * r4) - (r2 * r3)) " ) * (r1 * r4))) by A11, XCMPLX_0:def 7
.= (((r2 " ) * r2) * (((r1 * r4) - (r2 * r3)) " )) * (- r3)
.= (1 * (((r1 * r4) - (r2 * r3)) " )) * (- r3) by A13, XCMPLX_0:def 7
.= - ((((r1 * r4) - (r2 * r3)) " ) * r3) ;
hence w2 = (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) by A15, Th6; :: thesis: verum

end;

set a4 = (((r1 * r4) - (r2 * r3)) " ) * r1;
set a3 = - ((((r1 * r4) - (r2 * r3)) " ) * r3);
set a2 = - ((((r1 * r4) - (r2 * r3)) " ) * r2);
set a1 = (((r1 * r4) - (r2 * r3)) " ) * r4;

now

assume A16: r1 <> 0 ; :: thesis: ( w2 = (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) & w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2)) )
A17: (r1 " ) + ((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) = (r1 " ) * (1 + ((((r1 * r4) - (r2 * r3)) " ) * (r2 * r3)))
.= (r1 " ) * (((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) + ((((r1 * r4) - (r2 * r3)) " ) * (r2 * r3))) by A11, XCMPLX_0:def 7
.= (((r1 * r4) - (r2 * r3)) " ) * (((r1 " ) * r1) * r4)
.= (((r1 * r4) - (r2 * r3)) " ) * (1 * r4) by A16, XCMPLX_0:def 7
.= (((r1 * r4) - (r2 * r3)) " ) * r4 ;
(r1 " ) * v1 = ((r1 " ) * (r1 * w1)) + ((r1 " ) * (r2 * w2)) by A5, RLVECT_1:def 8
.= (((r1 " ) * r1) * w1) + ((r1 " ) * (r2 * w2)) by RLVECT_1:def 10
.= (1 * w1) + ((r1 " ) * (r2 * w2)) by A16, XCMPLX_0:def 7
.= w1 + ((r1 " ) * (r2 * w2)) by RLVECT_1:def 11
.= w1 + ((r2 * (r1 " )) * w2) by RLVECT_1:def 10 ;
then A18: w1 = ((r1 " ) * v1) - ((r2 * (r1 " )) * w2) by RLSUB_2:78;
then v2 = ((r3 * ((r1 " ) * v1)) - (r3 * ((r2 * (r1 " )) * w2))) + (r4 * w2) by A6, RLVECT_1:48
.= (((r3 * (r1 " )) * v1) - (r3 * (((r1 " ) * r2) * w2))) + (r4 * w2) by RLVECT_1:def 10
.= (((r3 * (r1 " )) * v1) - ((r3 * ((r1 " ) * r2)) * w2)) + (r4 * w2) by RLVECT_1:def 10
.= (((r3 * (r1 " )) * v1) - (((r1 " ) * (r3 * r2)) * w2)) + (r4 * w2)
.= ((((r1 " ) * r3) * v1) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def 10
.= (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2))) + (r4 * w2) by RLVECT_1:def 10 ;
then r1 * v2 = (r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + (r1 * (r4 * w2)) by RLVECT_1:def 8
.= (r1 * (((r1 " ) * (r3 * v1)) - ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def 10
.= ((r1 * ((r1 " ) * (r3 * v1))) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:48
.= (((r1 * (r1 " )) * (r3 * v1)) - (r1 * ((r1 " ) * ((r3 * r2) * w2)))) + ((r1 * r4) * w2) by RLVECT_1:def 10
.= (((r1 * (r1 " )) * (r3 * v1)) - ((r1 * (r1 " )) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def 10
.= ((1 * (r3 * v1)) - ((r1 * (r1 " )) * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def 7
.= ((1 * (r3 * v1)) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by A16, XCMPLX_0:def 7
.= ((r3 * v1) - (1 * ((r3 * r2) * w2))) + ((r1 * r4) * w2) by RLVECT_1:def 11
.= ((r3 * v1) - ((r3 * r2) * w2)) + ((r1 * r4) * w2) by RLVECT_1:def 11
.= (r3 * v1) - (((r3 * r2) * w2) - ((r1 * r4) * w2)) by RLVECT_1:43
.= (r3 * v1) + (- (((r3 * r2) - (r1 * r4)) * w2)) by RLVECT_1:49
.= (r3 * v1) + ((- ((r3 * r2) - (r1 * r4))) * w2) by Th6
.= (r3 * v1) + (((r1 * r4) - (r2 * r3)) * w2) ;
then (((r1 * r4) - (r2 * r3)) " ) * (r1 * v2) = ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) + ((((r1 * r4) - (r2 * r3)) " ) * (((r1 * r4) - (r2 * r3)) * w2)) by RLVECT_1:def 8
.= ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * ((r1 * r4) - (r2 * r3))) * w2) by RLVECT_1:def 10
.= ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) + (1 * w2) by A11, XCMPLX_0:def 7
.= ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) + w2 by RLVECT_1:def 11 ;
hence w2 = ((((r1 * r4) - (r2 * r3)) " ) * (r1 * v2)) - ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) by RLSUB_2:78
.= (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) - ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)) by RLVECT_1:def 10
.= (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1)) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) by RLVECT_1:def 10 ;
:: thesis: w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2))
hence w1 = ((r1 " ) * v1) - (((r2 * (r1 " )) * (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1))) + ((r2 * (r1 " )) * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by A18, RLVECT_1:def 8
.= ((r1 " ) * v1) - (((r2 * (r1 " )) * (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1))) + (((r2 * (r1 " )) * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - (((r2 * (r1 " )) * (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1))) + ((r2 * (((r1 " ) * r1) * (((r1 * r4) - (r2 * r3)) " ))) * v2))
.= ((r1 " ) * v1) - (((r2 * (r1 " )) * (- (((((r1 * r4) - (r2 * r3)) " ) * r3) * v1))) + ((r2 * (1 * (((r1 * r4) - (r2 * r3)) " ))) * v2)) by A16, XCMPLX_0:def 7
.= ((r1 " ) * v1) - (((r2 * (r1 " )) * (- ((((r1 * r4) - (r2 * r3)) " ) * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - (((r2 * (r1 " )) * ((- (((r1 * r4) - (r2 * r3)) " )) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by Th6
.= ((r1 " ) * v1) - ((((r2 * (r1 " )) * (- (((r1 * r4) - (r2 * r3)) " ))) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - ((((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * r2) * (r1 " )) * (r3 * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2))
.= ((r1 " ) * v1) - (((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * r2) * ((r1 " ) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - ((((- 1) * (((r1 * r4) - (r2 * r3)) " )) * (r2 * ((r1 " ) * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - (((- 1) * ((((r1 * r4) - (r2 * r3)) " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - ((- ((((r1 * r4) - (r2 * r3)) " ) * (r2 * ((r1 " ) * (r3 * v1))))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:29
.= ((r1 " ) * v1) - ((- (((((r1 * r4) - (r2 * r3)) " ) * r2) * ((r1 " ) * (r3 * v1)))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - ((- ((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * (r3 * v1))) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= ((r1 " ) * v1) - ((- (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1)) + ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2)) by RLVECT_1:def 10
.= (((r1 " ) * v1) - (- (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1))) - ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2) by RLVECT_1:41
.= (((r1 " ) * v1) + (((((((r1 * r4) - (r2 * r3)) " ) * r2) * (r1 " )) * r3) * v1)) - ((r2 * (((r1 * r4) - (r2 * r3)) " )) * v2) by RLVECT_1:30
.= (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + (- (((((r1 * r4) - (r2 * r3)) " ) * r2) * v2)) by A17, RLVECT_1:def 9 ;
:: thesis: verum

end;

then A19: ( w1 = (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1) + ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2) & w2 = ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2) ) by A7, A12, Th6;

now

let u be VECTOR of V; :: thesis: ( ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) & ( u in Lin {v1,v2} implies u in Lin {w1,w2} ) )
thus ( u in Lin {w1,w2} implies u in Lin {v1,v2} ) :: thesis: ( u in Lin {v1,v2} implies u in Lin {w1,w2} )

proof

assume u in Lin {w1,w2} ; :: thesis: u in Lin {v1,v2}
then consider r5, r6 being Real such that
A20: u = (r5 * w1) + (r6 * w2) by Th14;
u = ((r5 * (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + (r6 * (((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by A19, A20, RLVECT_1:def 8
.= ((r5 * (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1)) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 8
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (r5 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 10
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2)) + ((r6 * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + (r6 * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 10
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + (r6 * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 10
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2)) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 10
.= ((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + ((r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2))) by RLVECT_1:def 6
.= ((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (((r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2))) by RLVECT_1:def 6
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1)) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 6
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 9
.= (((r5 * ((((r1 * r4) - (r2 * r3)) " ) * r4)) + (r6 * (- ((((r1 * r4) - (r2 * r3)) " ) * r3)))) * v1) + (((r5 * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) + (r6 * ((((r1 * r4) - (r2 * r3)) " ) * r1))) * v2) by RLVECT_1:def 9 ;
hence u in Lin {v1,v2} by Th14; :: thesis: verum

end;

assume u in Lin {v1,v2} ; :: thesis: u in Lin {w1,w2}
then consider r5, r6 being Real such that
A21: u = (r5 * v1) + (r6 * v2) by Th14;
u = (r5 * ((r1 * w1) + (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by A5, A6, A21, RLVECT_1:def 8
.= ((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + ((r6 * (r3 * w1)) + (r6 * (r4 * w2))) by RLVECT_1:def 8
.= (((r5 * (r1 * w1)) + (r5 * (r2 * w2))) + (r6 * (r3 * w1))) + (r6 * (r4 * w2)) by RLVECT_1:def 6
.= (((r5 * (r1 * w1)) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 6
.= ((((r5 * r1) * w1) + (r6 * (r3 * w1))) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 10
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + (r5 * (r2 * w2))) + (r6 * (r4 * w2)) by RLVECT_1:def 10
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + (r6 * (r4 * w2)) by RLVECT_1:def 10
.= ((((r5 * r1) * w1) + ((r6 * r3) * w1)) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def 10
.= ((((r5 * r1) + (r6 * r3)) * w1) + ((r5 * r2) * w2)) + ((r6 * r4) * w2) by RLVECT_1:def 9
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) * w2) + ((r6 * r4) * w2)) by RLVECT_1:def 6
.= (((r5 * r1) + (r6 * r3)) * w1) + (((r5 * r2) + (r6 * r4)) * w2) by RLVECT_1:def 9 ;
hence u in Lin {w1,w2} by Th14; :: thesis: verum

end;

hence Lin {w1,w2} = Lin {v1,v2} by RLSUB_1:39; :: thesis: ( {w1,w2} is linearly-independent & w1 <> w2 )

now

let a, b be Real; :: thesis: ( (a * w1) + (b * w2) = 0. V implies ( not a <> 0 & not b <> 0 ) )
A22: ((r1 * r4) - (r2 * r3)) " <> 0 by A11, XCMPLX_1:203;
assume (a * w1) + (b * w2) = 0. V ; :: thesis: ( not a <> 0 & not b <> 0 )
then A23: 0. V = ((a * (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + (b * (((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1) + (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by A19, RLVECT_1:def 8
.= ((a * (((((r1 * r4) - (r2 * r3)) " ) * r4) * v1)) + (a * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 8
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + (b * (((((r1 * r4) - (r2 * r3)) " ) * r1) * v2))) by RLVECT_1:def 10
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + ((b * ((- ((((r1 * r4) - (r2 * r3)) " ) * r3)) * v1)) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 10
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (a * ((- ((((r1 * r4) - (r2 * r3)) " ) * r2)) * v2))) + (((b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 10
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2)) + (((b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 10
.= ((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + (((b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2))) by RLVECT_1:def 6
.= ((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + (((b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2))) by RLVECT_1:def 6
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) * v1) + ((b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3))) * v1)) + (((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 6
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) * v2) + ((b * ((((r1 * r4) - (r2 * r3)) " ) * r1)) * v2)) by RLVECT_1:def 9
.= (((a * ((((r1 * r4) - (r2 * r3)) " ) * r4)) + (b * (- ((((r1 * r4) - (r2 * r3)) " ) * r3)))) * v1) + (((a * (- ((((r1 * r4) - (r2 * r3)) " ) * r2))) + (b * ((((r1 * r4) - (r2 * r3)) " ) * r1))) * v2) by RLVECT_1:def 9 ;
then 0 = (((r1 * r4) - (r2 * r3)) " ) * ((r4 * a) + ((- r3) * b)) by A1, A2, RLVECT_3:14;
then A24: (r4 * a) - (r3 * b) = 0 by A22, XCMPLX_1:6;
0 = (((r1 * r4) - (r2 * r3)) " ) * (((- r2) * a) + (r1 * b)) by A1, A2, A23, RLVECT_3:14;
then A25: (r1 * b) + (- (r2 * a)) = 0 by A22, XCMPLX_1:6;
assume A26: ( a <> 0 or b <> 0 ) ; :: thesis: contradiction

now

per cases ( a <> 0 or b <> 0 ) by A26;

suppose A27: a <> 0 ; :: thesis: contradiction

(a " ) * (r1 * b) = ((a " ) * a) * r2 by A25, XCMPLX_1:4;
then (a " ) * (r1 * b) = 1 * r2 by A27, XCMPLX_0:def 7;
then r2 = r1 * ((a " ) * b) ;
then v1 = (r1 * w1) + (r1 * (((a " ) * b) * w2)) by A5, RLVECT_1:def 10;
then A28: v1 = r1 * (w1 + (((a " ) * b) * w2)) by RLVECT_1:def 8;
((a " ) * a) * r4 = (a " ) * (r3 * b) by A24, XCMPLX_1:4;
then 1 * r4 = (a " ) * (r3 * b) by A27, XCMPLX_0:def 7;
then r4 = r3 * ((a " ) * b) ;
then v2 = (r3 * w1) + (r3 * (((a " ) * b) * w2)) by A6, RLVECT_1:def 10;
then v2 = r3 * (w1 + (((a " ) * b) * w2)) by RLVECT_1:def 8;
hence contradiction by A1, A2, A28, Th24; :: thesis: verum

end;

suppose A29: b <> 0 ; :: thesis: contradiction

((b " ) * b) * r1 = (b " ) * (r2 * a) by A25, XCMPLX_1:4;
then 1 * r1 = (b " ) * (r2 * a) by A29, XCMPLX_0:def 7;
then r1 = r2 * ((b " ) * a) ;
then v1 = (r2 * (((b " ) * a) * w1)) + (r2 * w2) by A5, RLVECT_1:def 10;
then A30: v1 = r2 * ((((b " ) * a) * w1) + w2) by RLVECT_1:def 8;
((b " ) * b) * r3 = (b " ) * (r4 * a) by A24, XCMPLX_1:4;
then 1 * r3 = (b " ) * (r4 * a) by A29, XCMPLX_0:def 7;
then r3 = r4 * ((b " ) * a) ;
then v2 = (r4 * (((b " ) * a) * w1)) + (r4 * w2) by A6, RLVECT_1:def 10;
then v2 = r4 * ((((b " ) * a) * w1) + w2) by RLVECT_1:def 8;
hence contradiction by A1, A2, A30, Th24; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence ( {w1,w2} is linearly-independent & w1 <> w2 ) by RLVECT_3:14; :: thesis: verum