let f be Function; for O being non empty connected Poset
for T being non empty array of O
for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let O be non empty connected Poset; for T being non empty array of O
for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let T be non empty array of O; for p, q, r being Element of dom T st r in p & f = Swap ((id (dom T)),p,q) holds
( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
let p, q, r be Element of dom T; ( r in p & f = Swap ((id (dom T)),p,q) implies ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] ) )
assume that
A1:
r in p
and
A2:
f = Swap ((id (dom T)),p,q)
; ( ((T,p,q) incl) . (r,q) = [(f . r),(f . q)] & ((T,p,q) incl) . (r,p) = [(f . r),(f . p)] )
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
;
then A3:
dom (Swap ((id (dom T)),p,q)) = dom T
by FUNCT_7:99;
not p c= r
by A1, ORDINAL6:4;
then
( r nin {p} & r nin (succ q) \ p )
by Th59, TARSKI:def 1;
then
( [r,p] nin [:{p},((succ q) \ p):] & [r,p] nin [:((succ q) \ p),{q}:] & [r,q] nin [:{p},((succ q) \ p):] & [r,q] nin [:((succ q) \ p),{q}:] )
by ZFMISC_1:87;
then A4:
( [r,q] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) & [r,p] nin dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) )
by XBOOLE_0:def 3;
hence ((T,p,q) incl) . (r,q) =
[:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,q)
by FUNCT_4:11
.=
[(f . r),(f . q)]
by A2, A3, FUNCT_3:def 8
;
((T,p,q) incl) . (r,p) = [(f . r),(f . p)]
thus ((T,p,q) incl) . (r,p) =
[:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] . (r,p)
by A4, FUNCT_4:11
.=
[(f . r),(f . p)]
by A2, A3, FUNCT_3:def 8
; verum