let F be Field; :: thesis: for e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] holds
( ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
let e, f, g, h be Element of [: the carrier of F, the carrier of F, the carrier of F:]; :: thesis: ( ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) )
A1: ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F & ( for K being Element of F holds
( not K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) or not K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) or not K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ) implies ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

proof

assume that
A2: (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F and
A3: (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F and
A4: (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

now :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

A5: now :: thesis: ( (e `3_3) - (f `3_3) <> 0. F & ( for K being Element of F holds
( not K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) or not K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) or not K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ) implies ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

assume A6: (e `3_3) - (f `3_3) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A7: (((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `3_3) - (f `3_3)) = ((g `3_3) - (h `3_3)) * ((((e `3_3) - (f `3_3)) ") * ((e `3_3) - (f `3_3))) by GROUP_1:def 3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A6, VECTSP_1:def 10
.= (g `3_3) - (h `3_3) by VECTSP_1:def 8 ;
A8: (((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `2_3) - (f `2_3)) = (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) * (((e `3_3) - (f `3_3)) ") by GROUP_1:def 3
.= (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) * (((e `3_3) - (f `3_3)) ") by A4, Lm1
.= ((g `2_3) - (h `2_3)) * (((e `3_3) - (f `3_3)) * (((e `3_3) - (f `3_3)) ")) by GROUP_1:def 3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A6, VECTSP_1:def 10
.= (g `2_3) - (h `2_3) by VECTSP_1:def 8 ;
(((g `3_3) - (h `3_3)) * (((e `3_3) - (f `3_3)) ")) * ((e `1_3) - (f `1_3)) = (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) * (((e `3_3) - (f `3_3)) ") by GROUP_1:def 3
.= (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) * (((e `3_3) - (f `3_3)) ") by A3, Lm1
.= ((g `1_3) - (h `1_3)) * (((e `3_3) - (f `3_3)) * (((e `3_3) - (f `3_3)) ")) by GROUP_1:def 3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A6, VECTSP_1:def 10
.= (g `1_3) - (h `1_3) by VECTSP_1:def 8 ;
hence ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A8, A7; :: thesis: verum

end;

A9: now :: thesis: ( (e `2_3) - (f `2_3) <> 0. F & ( for K being Element of F holds
( not K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) or not K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) or not K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ) implies ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

assume A10: (e `2_3) - (f `2_3) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A11: (((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `2_3) - (f `2_3)) = ((g `2_3) - (h `2_3)) * ((((e `2_3) - (f `2_3)) ") * ((e `2_3) - (f `2_3))) by GROUP_1:def 3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A10, VECTSP_1:def 10
.= (g `2_3) - (h `2_3) by VECTSP_1:def 8 ;
A12: (((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `3_3) - (f `3_3)) = (((e `2_3) - (f `2_3)) ") * (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) by GROUP_1:def 3
.= (((e `2_3) - (f `2_3)) ") * (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) by A4, Lm1
.= ((((e `2_3) - (f `2_3)) ") * ((e `2_3) - (f `2_3))) * ((g `3_3) - (h `3_3)) by GROUP_1:def 3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A10, VECTSP_1:def 10
.= (g `3_3) - (h `3_3) by VECTSP_1:def 8 ;
(((g `2_3) - (h `2_3)) * (((e `2_3) - (f `2_3)) ")) * ((e `1_3) - (f `1_3)) = (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) * (((e `2_3) - (f `2_3)) ") by GROUP_1:def 3
.= (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) * (((e `2_3) - (f `2_3)) ") by A2, Lm1
.= ((g `1_3) - (h `1_3)) * (((e `2_3) - (f `2_3)) * (((e `2_3) - (f `2_3)) ")) by GROUP_1:def 3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A10, VECTSP_1:def 10
.= (g `1_3) - (h `1_3) by VECTSP_1:def 8 ;
hence ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A11, A12; :: thesis: verum

end;

now :: thesis: ( (e `1_3) - (f `1_3) <> 0. F & ( for K being Element of F holds
( not K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) or not K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) or not K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ) implies ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )

assume A13: (e `1_3) - (f `1_3) <> 0. F ; :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) )
A14: (((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `1_3) - (f `1_3)) = ((g `1_3) - (h `1_3)) * ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) by GROUP_1:def 3
.= ((g `1_3) - (h `1_3)) * (1_ F) by A13, VECTSP_1:def 10
.= (g `1_3) - (h `1_3) by VECTSP_1:def 8 ;
A15: (((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `3_3) - (f `3_3)) = (((e `1_3) - (f `1_3)) ") * (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) by GROUP_1:def 3
.= (((e `1_3) - (f `1_3)) ") * (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) by A3, Lm1
.= ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) * ((g `3_3) - (h `3_3)) by GROUP_1:def 3
.= ((g `3_3) - (h `3_3)) * (1_ F) by A13, VECTSP_1:def 10
.= (g `3_3) - (h `3_3) by VECTSP_1:def 8 ;
(((g `1_3) - (h `1_3)) * (((e `1_3) - (f `1_3)) ")) * ((e `2_3) - (f `2_3)) = (((e `1_3) - (f `1_3)) ") * (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) by GROUP_1:def 3
.= (((e `1_3) - (f `1_3)) ") * (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) by A2, Lm1
.= ((((e `1_3) - (f `1_3)) ") * ((e `1_3) - (f `1_3))) * ((g `2_3) - (h `2_3)) by GROUP_1:def 3
.= ((g `2_3) - (h `2_3)) * (1_ F) by A13, VECTSP_1:def 10
.= (g `2_3) - (h `2_3) by VECTSP_1:def 8 ;
hence ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A14, A15; :: thesis: verum

end;

hence ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) by A9, A5; :: thesis: verum

end;

hence ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ; :: thesis: verum

end;

( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )

proof

A16: now :: thesis: ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )

given K being Element of F such that A17: K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) and
A18: ( K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) ; :: thesis: ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )
A19: (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = ((K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (f `3_3))) - ((K * ((e `2_3) - (f `2_3))) * ((e `3_3) - (f `3_3))) by A18, GROUP_1:def 3;
( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = ((K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (f `2_3))) - ((K * ((e `1_3) - (f `1_3))) * ((e `2_3) - (f `2_3))) & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = ((K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (f `3_3))) - ((K * ((e `1_3) - (f `1_3))) * ((e `3_3) - (f `3_3))) ) by A17, A18, GROUP_1:def 3;
hence ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) by A19, RLVECT_1:15; :: thesis: verum

end;

A20: now :: thesis: ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F & ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )

assume that
A21: (e `1_3) - (f `1_3) = 0. F and
A22: (e `2_3) - (f `2_3) = 0. F and
A23: (e `3_3) - (f `3_3) = 0. F ; :: thesis: ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) )
A24: ((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3)) = 0. F by A23, VECTSP_1:7;
( ((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3)) = 0. F & ((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3)) = 0. F ) by A21, VECTSP_1:7;
hence ( ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) implies ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) ) by A21, A22, A24, RLVECT_1:15; :: thesis: verum

end;

assume ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ; :: thesis: ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F )
hence ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) by A20, A16; :: thesis: verum

end;

hence ( ( (((e `1_3) - (f `1_3)) * ((g `2_3) - (h `2_3))) - (((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((g `3_3) - (h `3_3))) - (((g `1_3) - (h `1_3)) * ((e `3_3) - (f `3_3))) = 0. F & (((e `2_3) - (f `2_3)) * ((g `3_3) - (h `3_3))) - (((g `2_3) - (h `2_3)) * ((e `3_3) - (f `3_3))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1_3) - (f `1_3)) = (g `1_3) - (h `1_3) & K * ((e `2_3) - (f `2_3)) = (g `2_3) - (h `2_3) & K * ((e `3_3) - (f `3_3)) = (g `3_3) - (h `3_3) ) or ( (e `1_3) - (f `1_3) = 0. F & (e `2_3) - (f `2_3) = 0. F & (e `3_3) - (f `3_3) = 0. F ) ) ) by A1; :: thesis: verum