let f be Function; :: thesis: for O being non empty connected Poset
for T being non empty array of O
for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let O be non empty connected Poset; :: thesis: for T being non empty array of O
for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let T be non empty array of O; :: thesis: for q, r, p being Element of dom T st q in r & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
let q, r, p be Element of dom T; :: thesis: ( q in r & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] ) )
assume that
Z0: q in r and
Z1: f = Swap ((id (dom T)),p,q) ; :: thesis: ( ((T,p,q) incl) . (p,r) = [(f . p),(f . r)] & ((T,p,q) incl) . (q,r) = [(f . q),(f . r)] )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set h = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):];
set Y = (succ q) \ p;
set Z1 = [:{p},((succ q) \ p):];
set Z2 = [:((succ q) \ p),{q}:];
set g = id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]);
dom (id (dom T)) = dom T by RELAT_1:45;
then A4: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99;
not r c= q by Z0, ORDINAL6:4;
then ( r nin {q} & r nin (succ q) \ p ) by TT, TARSKI:def 1;
then ( [p,r] nin [:{p},((succ q) \ p):] & [p,r] nin [:((succ q) \ p),{q}:] & [q,r] nin [:{p},((succ q) \ p):] & [q,r] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87;
then A3: ( [p,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [q,r] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) ) by XBOOLE_0:def 3;
hence ((T,p,q) incl) . (p,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (p,r) by FUNCT_4:11
.= [(f . p),(f . r)] by Z1, A4, FUNCT_3:def 8 ;
:: thesis: ((T,p,q) incl) . (q,r) = [(f . q),(f . r)]
thus ((T,p,q) incl) . (q,r) = [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (q,r) by A3, FUNCT_4:11
.= [(f . q),(f . r)] by Z1, A4, FUNCT_3:def 8 ; :: thesis: verum