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;
now :: thesis: for i being object st i in A holds
(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;
hence doms f = A --> B by PBOOLE:3; :: thesis: verum