let f be Function; :: thesis: for O being non empty connected Poset
for T being non empty array of O
for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let O be non empty connected Poset; :: thesis: for T being non empty array of O
for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let T be non empty array of O; :: thesis: for r, p, s, q being Element of dom T st r <> p & s <> q & f = Swap ((id (dom T)),p,q) holds
((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
let r, p, s, q be Element of dom T; :: thesis: ( r <> p & s <> q & f = Swap ((id (dom T)),p,q) implies ((T,p,q) incl) . (r,s) = [(f . r),(f . s)] )
assume that
Z0: ( r <> p & s <> q ) and
Z1: f = Swap ((id (dom T)),p,q) ; :: thesis: ((T,p,q) incl) . (r,s) = [(f . r),(f . s)]
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}:]);
A0: dom f = dom (id (dom T)) by Z1, FUNCT_7:99
.= dom T by RELAT_1:45 ;
( r nin {p} & s nin {q} ) by Z0, TARSKI:def 1;
then ( [r,s] nin [:{p},((succ q) \ p):] & [r,s] nin [:((succ q) \ p),{q}:] ) by ZFMISC_1:87;
then [r,s] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) by XBOOLE_0:def 3;
hence ((T,p,q) incl) . (r,s) = [:f,f:] . (r,s) by Z1, FUNCT_4:11
.= [(f . r),(f . s)] by A0, FUNCT_3:def 8 ;
:: thesis: verum