let F be Field; :: thesis: for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b
let a, b, p, q, r, s be Element of (MPS F); :: thesis: ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b )
defpred S₁[ Element of H₁(F), Element of H₁(F), Element of H₁(F), Element of H₁(F)] means ( ((($1 `1_3) - ($2 `1_3)) * (($3 `2_3) - ($4 `2_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `2_3) - ($2 `2_3))) = 0. F & ((($1 `1_3) - ($2 `1_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `1_3) - ($4 `1_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F & ((($1 `2_3) - ($2 `2_3)) * (($3 `3_3) - ($4 `3_3))) - ((($3 `2_3) - ($4 `2_3)) * (($1 `3_3) - ($2 `3_3))) = 0. F );
assume that
A1: a,b '||' p,q and
A2: a,b '||' r,s ; :: thesis: ( p,q '||' r,s or a = b )
consider e, f, g, h being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A3: [[e,f],[g,h]] = [[a,b],[p,q]] and
A4: S₁[e,f,g,h] by A1, Th12;
consider i, j, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A5: [[i,j],[k,l]] = [[a,b],[r,s]] and
A6: S₁[i,j,k,l] by A2, Th12;
A7: ( i = a & j = b ) by A5, MCART_1:93;
A8: ( k = r & l = s ) by A5, MCART_1:93;
set A = (e `1_3) - (f `1_3);
set B = (e `2_3) - (f `2_3);
set C = (e `3_3) - (f `3_3);
set D = (g `1_3) - (h `1_3);
set E = (g `2_3) - (h `2_3);
set K = (g `3_3) - (h `3_3);
set G = (k `1_3) - (l `1_3);
set H = (k `2_3) - (l `2_3);
set I = (k `3_3) - (l `3_3);
A9: ( e = a & f = b ) by A3, MCART_1:93;
A10: ( g = p & h = q ) by A3, MCART_1:93;

now :: thesis: ( a <> b implies ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[g,h],[k,l]] = [[p,q],[r,s]] & S₁[g,h,k,l] ) )

assume A11: a <> b ; :: thesis: ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[g,h],[k,l]] = [[p,q],[r,s]] & S₁[g,h,k,l] )

now :: thesis: ( ( (e `1_3) - (f `1_3) <> 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F ) or ( (e `2_3) - (f `2_3) <> 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F ) or ( (e `3_3) - (f `3_3) <> 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F ) )

AA: for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds x = [(x `1_3),(x `2_3),(x `3_3)] ;
e = [(e `1_3),(e `2_3),(e `3_3)] ;
then A12: ( e `1_3 <> f `1_3 or e `2_3 <> f `2_3 or e `3_3 <> f `3_3 ) by A9, A11, AA;

per cases ( (e `1_3) - (f `1_3) <> 0. F or (e `2_3) - (f `2_3) <> 0. F or (e `3_3) - (f `3_3) <> 0. F ) by A12, RLVECT_1:21;

case A13: (e `1_3) - (f `1_3) <> 0. F ; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F )

hence (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, Lm4; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F )
thus A14: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A13, Lm4; :: thesis: (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F
( ((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) = ((((g `1_3) - (h `1_3)) * ((e `2_3) - (f `2_3))) * (((e `1_3) - (f `1_3)) ")) * ((k `3_3) - (l `3_3)) & ((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3)) = ((((k `1_3) - (l `1_3)) * ((e `2_3) - (f `2_3))) * (((e `1_3) - (f `1_3)) ")) * ((g `3_3) - (h `3_3)) ) by A4, A6, A9, A7, A13, VECTSP_1:30;
hence (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A14, Lm8; :: thesis: verum

end;

case A15: (e `2_3) - (f `2_3) <> 0. F ; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )

hence (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis: ( (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
thus A16: (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A15, Lm4; :: thesis: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F
( ((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) = ((((g `2_3) - (h `2_3)) * ((e `1_3) - (f `1_3))) * (((e `2_3) - (f `2_3)) ")) * ((k `3_3) - (l `3_3)) & ((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3)) = ((((k `2_3) - (l `2_3)) * ((e `1_3) - (f `1_3))) * (((e `2_3) - (f `2_3)) ")) * ((g `3_3) - (h `3_3)) ) by A4, A6, A9, A7, A15, VECTSP_1:30;
hence (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A16, Lm8; :: thesis: verum

end;

case A17: (e `3_3) - (f `3_3) <> 0. F ; :: thesis: ( (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )

hence (((g `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, Lm6; :: thesis: ( (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F & (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F )
A18: ( ((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) = ((((g `3_3) - (h `3_3)) * ((e `1_3) - (f `1_3))) * (((e `3_3) - (f `3_3)) ")) * ((k `2_3) - (l `2_3)) & ((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3)) = ((((k `3_3) - (l `3_3)) * ((e `1_3) - (f `1_3))) * (((e `3_3) - (f `3_3)) ")) * ((g `2_3) - (h `2_3)) ) by A4, A6, A9, A7, A17, VECTSP_1:30;
(((g `3_3) - (h `3_3)) * ((k `2_3) - (l `2_3))) - (((k `3_3) - (l `3_3)) * ((g `2_3) - (h `2_3))) = 0. F by A4, A6, A9, A7, A17, Lm6;
hence (((g `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((g `2_3) - (h `2_3))) = 0. F by A18, Lm8; :: thesis: (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F
thus (((g `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((g `3_3) - (h `3_3))) = 0. F by A4, A6, A9, A7, A17, Lm6; :: thesis: verum

end;

end;

end;

hence ex g, h, k, l being Element of [: the carrier of F, the carrier of F, the carrier of F:] st
( [[g,h],[k,l]] = [[p,q],[r,s]] & S₁[g,h,k,l] ) by A10, A8; :: thesis: verum

end;

hence ( p,q '||' r,s or a = b ) by Th12; :: thesis: verum