let O be non empty connected Poset; for T being non empty array of O
for p, q being Element of dom T holds
( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
let T be non empty array of O; for p, q being Element of dom T holds
( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
let p, q be Element of dom T; ( dom ((T,p,q) incl) = [:(dom T),(dom T):] & rng ((T,p,q) incl) c= [:(dom T),(dom T):] )
set X = dom T;
set i = id (dom T);
set s = Swap ((id (dom T)),p,q);
set f = [:(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 A1:
dom (Swap ((id (dom T)),p,q)) = dom T
by FUNCT_7:99;
A2:
( {p} c= dom T & {q} c= dom T & (succ q) \ p c= dom T )
by Th60, ZFMISC_1:31;
A3: [:(dom T),(dom T):] \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:]) =
([:(dom T),(dom T):] \/ [:{p},((succ q) \ p):]) \/ [:((succ q) \ p),{q}:]
by XBOOLE_1:4
.=
[:(dom T),(dom T):] \/ [:((succ q) \ p),{q}:]
by A2, XBOOLE_1:12, ZFMISC_1:96
.=
[:(dom T),(dom T):]
by A2, XBOOLE_1:12, ZFMISC_1:96
;
thus dom ((T,p,q) incl) =
(dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ (dom (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])))
by FUNCT_4:def 1
.=
(dom [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):]) \/ ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])
.=
[:(dom T),(dom T):]
by A1, A3, FUNCT_3:def 8
; rng ((T,p,q) incl) c= [:(dom T),(dom T):]
A4:
( rng (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & rng (id (dom T)) = dom T )
;
rng (Swap ((id (dom T)),p,q)) = dom T
by A4, FUNCT_7:103;
then
rng [:(Swap ((id (dom T)),p,q)),(Swap ((id (dom T)),p,q)):] = [:(dom T),(dom T):]
by FUNCT_3:67;
hence
rng ((T,p,q) incl) c= [:(dom T),(dom T):]
by A3, A4, FUNCT_4:17; verum