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:11;
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, Th23;
hence Frege f is Function of (Funcs A,B),(Funcs A,C) by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum