let O be non empty connected Poset; :: thesis: for T being non empty array of O
for p, q, s being Element of dom T st p in q & q in s holds
( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
let T be non empty array of O; :: thesis: for p, q, s being Element of dom T st p in q & q in s holds
( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
let p, q, s be Element of dom T; :: thesis: ( p in q & q in s implies ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] ) )
assume Z0: ( p in q & q in s ) ; :: thesis: ( ((T,p,q) incl) . (p,s) = [q,s] & ((T,p,q) incl) . (q,s) = [p,s] )
set X = dom T;
set i = id (dom T);
set f = 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;
A0: dom (id (dom T)) = dom T by RELAT_1:45;
A2: ( s <> p & s <> q ) by Z0;
thus ((T,p,q) incl) . (p,s) = [((Swap ((id (dom T)),p,q)) . p),((Swap ((id (dom T)),p,q)) . s)] by Z0, FF7
.= [((Swap ((id (dom T)),p,q)) . p),((id (dom T)) . s)] by A2, TSc
.= [((Swap ((id (dom T)),p,q)) . p),s] by FUNCT_1:17
.= [((id (dom T)) . q),s] by A0, TSa
.= [q,s] by FUNCT_1:17 ; :: thesis: ((T,p,q) incl) . (q,s) = [p,s]
thus ((T,p,q) incl) . (q,s) = [((Swap ((id (dom T)),p,q)) . q),((Swap ((id (dom T)),p,q)) . s)] by Z0, FF7
.= [((Swap ((id (dom T)),p,q)) . q),((id (dom T)) . s)] by A2, TSc
.= [((Swap ((id (dom T)),p,q)) . q),s] by FUNCT_1:17
.= [((id (dom T)) . p),s] by A0, TSb
.= [p,s] by FUNCT_1:17 ; :: thesis: verum