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

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