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 A1: ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs B,C) holds doms f = A --> B
let f be Function of A,(Funcs B,C); :: thesis: doms f = A --> B
A2: ( Funcs B,C = {} implies A = {} ) by A1, FUNCT_2:11;
then dom f = A by FUNCT_2:def 1;
then reconsider g = f as ManySortedFunction of by PARTFUN1:def 4;

now

let i be set ; :: thesis: ( i in A implies (doms g) . i = (A --> B) . i )
assume A3: i in A ; :: thesis: (doms g) . i = (A --> B) . i
then A4: g . i in Funcs B,C by A2, FUNCT_2:7;
thus (doms g) . i = dom (g . i) by A3, MSSUBFAM:14
.= B by A4, FUNCT_2:169
.= (A --> B) . i by A3, FUNCOP_1:13 ; :: thesis: verum

end;

hence doms f = A --> B by PBOOLE:3; :: thesis: verum