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 () = A

let A be set ; :: thesis: for B being V2() ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom () = A

let B be V2() ManySortedSet of I; :: thesis: for F being ManySortedFunction of I --> A,B holds dom () = A
let F be ManySortedFunction of I --> A,B; :: thesis: dom () = 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 () = 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:
then consider i being object such that
A4: ( i in I & x = F . i ) by ;
( (I --> A) . i = A & x is Function of ((I --> A) . i),(B . i) ) by ;
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 ;
commute F = curry' () by FUNCT_6:def 10
.= {} by ;
hence dom () = A by A3; :: thesis: verum
end;
suppose A6: not A is empty ; :: thesis: dom () = 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 ;
then reconsider x9 = x as Function of A,(B . i) by ;
B . i in rng B by ;
then ( rng x9 c= B . i & B . i c= union (rng B) ) by ;
then A9: rng x9 c= union (rng B) ;
dom x9 = A by ;
hence x in Funcs (A,(union (rng B))) by ; :: thesis: verum
end;
then F in Funcs (I,(Funcs (A,(union (rng B))))) by ;
then commute F in Funcs (A,(Funcs (I,(union (rng B))))) by ;
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 () = A by ; :: thesis: verum
end;
end;