let A, B, C be set ; :: thesis: ( ( not C = {} or B = {} or A = {} ) implies for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) )

assume A1: ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C))

then A2: ( Funcs (A,C) = {} implies Funcs (A,B) = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: Frege f is Function of (Funcs (A,B)),(Funcs (A,C))

( dom (Frege f) = Funcs (A,B) & rng (Frege f) c= Funcs (A,C) ) by A1, Th21, Th22;

hence Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum

assume A1: ( not C = {} or B = {} or A = {} ) ; :: thesis: for f being Function of A,(Funcs (B,C)) holds Frege f is Function of (Funcs (A,B)),(Funcs (A,C))

then A2: ( Funcs (A,C) = {} implies Funcs (A,B) = {} ) by FUNCT_2:8;

let f be Function of A,(Funcs (B,C)); :: thesis: Frege f is Function of (Funcs (A,B)),(Funcs (A,C))

( dom (Frege f) = Funcs (A,B) & rng (Frege f) c= Funcs (A,C) ) by A1, Th21, Th22;

hence Frege f is Function of (Funcs (A,B)),(Funcs (A,C)) by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum