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 PBOOLE:def 3
.= product (A --> B) by A1, Th6
.= Funcs A,B by CARD_3:20 ; :: thesis: verum