let I be non empty set ; :: thesis: for A being set
for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let A be set ; :: thesis: for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A
let B be V2() 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 4;
A2: dom F = I by PARTFUN1:def 4;

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 set ; :: 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 set such that
A4: ( i in I & x = F . i ) by A2, FUNCT_1:def 5;
( (I --> A) . i = A & x is Function of ((I --> A) . i),(B . i) ) by A4, FUNCOP_1:13, PBOOLE:def 18;
then x = {} by A3;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

then rng F = {{} } by ZFMISC_1:39;
then A5: F = I --> {} by A2, FUNCOP_1:15;
commute F = curry' (uncurry F) by FUNCT_6:def 12
.= {} by A5, Th7, FUNCT_5:49 ;
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 set ; :: 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 set such that
A7: i in dom F and
A8: x = F . i by FUNCT_1:def 5;
(I --> A) . i = A by A2, A7, FUNCOP_1:13;
then reconsider x9 = x as Function of A,(B . i) by A2, A7, A8, PBOOLE:def 18;
B . i in rng B by A1, A2, A7, FUNCT_1:def 5;
then ( rng x9 c= B . i & B . i c= union (rng B) ) by RELAT_1:def 19, ZFMISC_1:92;
then A9: rng x9 c= union (rng B) by XBOOLE_1:1;
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:85;
then A10: commute F is Function of A,(Funcs I,(union (rng B))) by FUNCT_2:121;
not union (rng B) is empty by Th6;
then not Funcs I,(union (rng B)) is empty by FUNCT_2:11;
hence dom (commute F) = A by A10, FUNCT_2:def 1; :: thesis: verum

end;

end;