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: f is Function of A,B by FUNCT_2:66;
( B = {} implies A = {} ) by A2;
hence f . x in B by A1, A3, FUNCT_2:5; :: thesis: verum