let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q being Element of dom T st p in q holds
((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
let T be non empty array of O; :: thesis: for p, q being Element of dom T st p in q holds
((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
let p, q be Element of dom T; :: thesis: ( p in q implies ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one )
assume A1: p in q ; :: thesis: ((T,p,q) incl) | (inversions (Swap (T,p,q))) is one-to-one
set f = (T,p,q) incl ;
set s = Swap (T,p,q);
set w = inversions (Swap (T,p,q));
set fw = ((T,p,q) incl) | (inversions (Swap (T,p,q)));
A2: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not y in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y )
assume ( x in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) & y in dom (((T,p,q) incl) | (inversions (Swap (T,p,q)))) ) ; :: thesis: ( not (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y or x = y )
then A3: ( x in inversions (Swap (T,p,q)) & y in inversions (Swap (T,p,q)) ) by RELAT_1:57;
then consider x1, y1 being Element of dom T such that
A4: ( x = [x1,y1] & x1 in y1 & (Swap (T,p,q)) /. x1 > (Swap (T,p,q)) /. y1 ) by A2;
consider x2, y2 being Element of dom T such that
A5: ( y = [x2,y2] & x2 in y2 & (Swap (T,p,q)) /. x2 > (Swap (T,p,q)) /. y2 ) by A2, A3;
assume (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . x = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y ; :: thesis: x = y
then ((T,p,q) incl) . (x1,y1) = (((T,p,q) incl) | (inversions (Swap (T,p,q)))) . y by A4, A3, FUNCT_1:49
.= ((T,p,q) incl) . (x2,y2) by A5, A3, FUNCT_1:49 ;
then ( x1 = x2 & y1 = y2 ) by A1, A4, A5, Lm1;
hence x = y by A4, A5; :: thesis: verum