let A, B be set ; :: thesis: for f being Function st f in Funcs (A,B) holds
( dom f = A & rng f c= B )
let f be Function; :: thesis: ( f in Funcs (A,B) implies ( dom f = A & rng f c= B ) )
assume f in Funcs (A,B) ; :: thesis: ( dom f = A & rng f c= B )
then ex g being Function st
( f = g & dom g = A & rng g c= B ) by Def2;
hence ( dom f = A & rng f c= B ) ; :: thesis: verum