let I be non empty set ; :: thesis: for A being set
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let A be set ; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let F be ManySortedFunction of I --> A,B; :: thesis: dom (commute F) = A
A1: dom B = I by PARTFUN1:def 2;
A2: dom F = I by PARTFUN1:def 2;

per cases ( A is empty or not A is empty ) ;

suppose A3: A is empty ; :: thesis: dom (commute F) = A

rng F c= {{}}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in {{}} )
assume x in rng F ; :: thesis: x in {{}}
then consider i being object such that
A4: ( i in I & x = F . i ) by A2, FUNCT_1:def 3;
( (I --> A) . i = A & x is Function of ((I --> A) . i),(B . i) ) by A4, FUNCOP_1:7, PBOOLE:def 15;
then x = {} by A3;
hence x in {{}} by TARSKI:def 1; :: thesis: verum

end;

then rng F = {{}} by ZFMISC_1:33;
then A5: F = I --> {} by A2, FUNCOP_1:9;
commute F = curry' (uncurry F) by FUNCT_6:def 10
.= {} by A5, Th3, FUNCT_5:42 ;
hence dom (commute F) = A by A3; :: thesis: verum

end;

suppose A6: not A is empty ; :: thesis: dom (commute F) = A

rng F c= Funcs (A,(union (rng B)))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in Funcs (A,(union (rng B))) )
assume x in rng F ; :: thesis: x in Funcs (A,(union (rng B)))
then consider i being object such that
A7: i in dom F and
A8: x = F . i by FUNCT_1:def 3;
(I --> A) . i = A by A2, A7, FUNCOP_1:7;
then reconsider x9 = x as Function of A,(B . i) by A2, A7, A8, PBOOLE:def 15;
B . i in rng B by A1, A2, A7, FUNCT_1:def 3;
then ( rng x9 c= B . i & B . i c= union (rng B) ) by RELAT_1:def 19, ZFMISC_1:74;
then A9: rng x9 c= union (rng B) ;
dom x9 = A by A2, A7, FUNCT_2:def 1;
hence x in Funcs (A,(union (rng B))) by A9, FUNCT_2:def 2; :: thesis: verum

end;

then F in Funcs (I,(Funcs (A,(union (rng B))))) by A2, FUNCT_2:def 2;
then commute F in Funcs (A,(Funcs (I,(union (rng B))))) by A6, FUNCT_6:55;
then A10: commute F is Function of A,(Funcs (I,(union (rng B)))) by FUNCT_2:66;
not union (rng B) is empty by Th2;
then not Funcs (I,(union (rng B))) is empty by FUNCT_2:8;
hence dom (commute F) = A by A10, FUNCT_2:def 1; :: thesis: verum

end;

end;