let A, B, C be set ; :: thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs B,C) holds dom (Frege f) = Funcs A,B )
assume A1: ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs B,C) holds dom (Frege f) = Funcs A,B
let f be Function of A,(Funcs B,C); :: thesis: dom (Frege f) = Funcs A,B
thus dom (Frege f) = product (doms f) by PARTFUN1:def 4
.= product (A --> B) by A1, Th6
.= Funcs A,B by CARD_3:20 ; :: thesis: verum