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 2;

A2: dom F = I by PARTFUN1:def 2;

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 2;

A2: dom F = I by PARTFUN1:def 2;

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

end;

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

rng F c= {{}}

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;proof

then
rng F = {{}}
by ZFMISC_1:33;
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;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

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

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

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

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;proof

then
F in Funcs (I,(Funcs (A,(union (rng B)))))
by A2, FUNCT_2:def 2;
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;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

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