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 Z0: 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)));
A0: dom (Swap (T,p,q)) = dom T by FUNCT_7:99;
let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 (((T,p,q) incl) | (inversions (Swap (T,p,q)))) or not b₁ 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)))) . b₁ or x = b₁ )
let y be set ; :: 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 A1: ( 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
01: ( x = [x1,y1] & x1 in y1 & (Swap (T,p,q)) /. x1 > (Swap (T,p,q)) /. y1 ) by A0;
consider x2, y2 being Element of dom T such that
02: ( y = [x2,y2] & x2 in y2 & (Swap (T,p,q)) /. x2 > (Swap (T,p,q)) /. y2 ) by A0, A1;
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 01, A1, FUNCT_1:49
.= ((T,p,q) incl) . (x2,y2) by 02, A1, FUNCT_1:49 ;
then ( x1 = x2 & y1 = y2 ) by Z0, 01, 02, O2O;
hence x = y by 01, 02; :: thesis: verum