let A, B, x be set ; :: thesis: for f being Function st x in A & f in Funcs A,B holds
f . x in B
let f be Function; :: thesis: ( x in A & f in Funcs A,B implies f . x in B )
assume A1: x in A ; :: thesis: ( not f in Funcs A,B or f . x in B )
assume A2: f in Funcs A,B ; :: thesis: f . x in B
then A3: ( B = {} implies A = {} ) ;
f is Function of A,B by A2, FUNCT_2:121;
hence f . x in B by A1, A3, FUNCT_2:7; :: thesis: verum