consider X being non empty set such that
A1: X in B by SETFAM_1:def 10;
reconsider f = A --> X as Function of A,B by A1, FUNCOP_1:45;
take f ; :: thesis: f is non-empty
let n be object ; :: according to FUNCT_1:def 9 :: thesis: ( not n in dom f or not f . n is empty )
assume n in dom f ; :: thesis: not f . n is empty
then n in A by FUNCOP_1:13;
hence not f . n is empty by FUNCOP_1:7; :: thesis: verum