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