let F be Field; :: thesis: for a, b being Element of (MPS F) holds a,b '||' b,a
let a, b be Element of (MPS F); :: thesis: a,b '||' b,a
consider e, f being Element of [: the carrier of F, the carrier of F, the carrier of F:] such that
A1: [[e,f],[f,e]] = [[a,b],[b,a]] ;
A2: (((e `2_3) - (f `2_3)) * ((f `3_3) - (e `3_3))) - (((f `2_3) - (e `2_3)) * ((e `3_3) - (f `3_3))) = 0. F by Lm2;
( (((e `1_3) - (f `1_3)) * ((f `2_3) - (e `2_3))) - (((f `1_3) - (e `1_3)) * ((e `2_3) - (f `2_3))) = 0. F & (((e `1_3) - (f `1_3)) * ((f `3_3) - (e `3_3))) - (((f `1_3) - (e `1_3)) * ((e `3_3) - (f `3_3))) = 0. F ) by Lm2;
hence a,b '||' b,a by A1, A2, Th12; :: thesis: verum