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

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

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

end;

then rng F = {{} } by ZFMISC_1:39;
then A6: F = I --> {} by A1, FUNCOP_1:15;
commute F = curry' (uncurry F) by FUNCT_6:def 12
.= {} by A6, Th7, FUNCT_5:49 ;
hence dom (commute F) = A by A2; :: thesis: verum

end;

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

not union (rng B) is empty by Th6;
then A8: not Funcs I,(union (rng B)) is empty by FUNCT_2:11;
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
A9: ( i in dom F & x = F . i ) by FUNCT_1:def 5;
(I --> A) . i = A by A1, A9, FUNCOP_1:13;
then reconsider x' = x as Function of A,(B . i) by A1, A9, PBOOLE:def 18;
B . i <> {} by A1, A9;
then A10: ( dom x' = A & rng x' c= B . i ) by FUNCT_2:def 1, RELAT_1:def 19;
B . i in rng B by A1, A9, FUNCT_1:def 5;
then B . i c= union (rng B) by ZFMISC_1:92;
then rng x' c= union (rng B) by A10, XBOOLE_1:1;
hence x in Funcs A,(union (rng B)) by A10, FUNCT_2:def 2; :: thesis: verum

end;

then F in Funcs I,(Funcs A,(union (rng B))) by A1, FUNCT_2:def 2;
then commute F in Funcs A,(Funcs I,(union (rng B))) by A7, FUNCT_6:85;
then commute F is Function of A,(Funcs I,(union (rng B))) by FUNCT_2:121;
hence dom (commute F) = A by A8, FUNCT_2:def 1; :: thesis: verum

end;

end;