per cases ( C = {} or C <> {} ) ;

suppose A1: C = {} ; :: thesis: ~ f is Function of [:B,A:],C

then reconsider f = f as empty set ;
~ f = {} ;
hence ~ f is Function of [:B,A:],C by A1, Th1; :: thesis: verum

end;

suppose C <> {} ; :: thesis: ~ f is Function of [:B,A:],C

hence ~ f is Function of [:B,A:],C by FUNCT_4:49; :: thesis: verum

end;

end;