let O be non empty connected Poset; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 by RELAT_1:45;
then A0: dom (Swap ((id (dom T)),p,q)) = dom T by FUNCT_7:99;
A1: ( {p} c= dom T & {q} c= dom T & (succ q) \ p c= dom T ) by FF1, ZFMISC_1:31;
A2: [:(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 A1, XBOOLE_1:12, ZFMISC_1:96
.= [:(dom T),(dom T):] by A1, 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}:]) by RELAT_1:45
.= [:(dom T),(dom T):] by A0, A2, FUNCT_3:def 8 ; :: thesis: rng ((T,p,q) incl) c= [:(dom T),(dom T):]
A3: ( rng (id ([:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:])) = [:{p},((succ q) \ p):] \/ [:((succ q) \ p),{q}:] & rng (id (dom T)) = dom T ) by RELAT_1:45;
rng (Swap ((id (dom T)),p,q)) = dom T by A3, 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 A2, A3, FUNCT_4:17; :: thesis: verum