let F be Field; :: thesis: for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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 a, b, c, d be Element of (MPS F); :: thesis: ( a,b '||' c,d iff ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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: ( a,b '||' c,d implies ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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 ) ) ) )

proof

assume a,b '||' c,d ; :: thesis: ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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 ) ) )
then consider e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that
A2: [a,b,c,d] = [e,f,g,h] and
A3: ( (((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 PARSP_1:23;
( 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 A3, Lm3;
hence ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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 A2; :: thesis: verum

end;

( ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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 a,b '||' c,d )

proof

given e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] such that A4: [a,b,c,d] = [e,f,g,h] and
A5: ( 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: a,b '||' c,d
A6: (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F by A5, Lm3;
( (((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 ) by A5, Lm3;
hence a,b '||' c,d by A4, A6, PARSP_1:23; :: thesis: verum

end;

hence ( a,b '||' c,d iff ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & ( 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