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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F & (((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F & (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `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) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F & (((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F & (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F ) iff ( ex K being Element of F st
( K * ((e `1) - (f `1)) = (g `1) - (h `1) & K * ((e `2) - (f `2)) = (g `2) - (h `2) & K * ((e `3) - (f `3)) = (g `3) - (h `3) ) or ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) ) )
A1: ( (((e `1) - (f `1)) * ((g `2) - (h `2))) - (((g `1) - (h `1)) * ((e `2) - (f `2))) = 0. F & (((e `1) - (f `1)) * ((g `3) - (h `3))) - (((g `1) - (h `1)) * ((e `3) - (f `3))) = 0. F & (((e `2) - (f `2)) * ((g `3) - (h `3))) - (((g `2) - (h `2)) * ((e `3) - (f `3))) = 0. F & ( for K being Element of F holds
( not K * ((e `1) - (f `1)) = (g `1) - (h `1) or not K * ((e `2) - (f `2)) = (g `2) - (h `2) or not K * ((e `3) - (f `3)) = (g `3) - (h `3) ) ) implies ( (e `1) - (f `1) = 0. F & (e `2) - (f `2) = 0. F & (e `3) - (f `3) = 0. F ) )

proof

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

now

A5: now

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

end;

A9: now

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

end;

now

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

end;

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

end;

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

end;

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

proof

A16: now

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

end;

A20: now

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

end;

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

end;

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