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 2
.= product (A --> B) by A1, Th5
.= Funcs (A,B) by CARD_3:11 ; :: thesis: verum