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]] & (((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 ) )
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]] & (((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 ) )
[[a,b],[c,d]] in 4C_3 F ;
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]] & (((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 Th9; :: thesis: verum