let A, B, C be set ; :: thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds doms f = A --> B )

assume ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds doms f = A --> B

then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: doms f = A --> B

reconsider g = f as ManySortedFunction of A by A1;

assume ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds doms f = A --> B

then A1: ( Funcs (B,C) = {} implies A = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: doms f = A --> B

reconsider g = f as ManySortedFunction of A by A1;

now :: thesis: for i being object st i in A holds

(doms g) . i = (A --> B) . i

hence
doms f = A --> B
by PBOOLE:3; :: thesis: verum(doms g) . i = (A --> B) . i

let i be object ; :: thesis: ( i in A implies (doms g) . i = (A --> B) . i )

assume A2: i in A ; :: thesis: (doms g) . i = (A --> B) . i

then A3: g . i in Funcs (B,C) by A1, FUNCT_2:5;

thus (doms g) . i = dom (g . i) by A2, MSSUBFAM:14

.= B by A3, FUNCT_2:92

.= (A --> B) . i by A2, FUNCOP_1:7 ; :: thesis: verum

end;assume A2: i in A ; :: thesis: (doms g) . i = (A --> B) . i

then A3: g . i in Funcs (B,C) by A1, FUNCT_2:5;

thus (doms g) . i = dom (g . i) by A2, MSSUBFAM:14

.= B by A3, FUNCT_2:92

.= (A --> B) . i by A2, FUNCOP_1:7 ; :: thesis: verum