consider X being non empty set such that
A1: X in B by SETFAM_1:def 11;
reconsider f = A --> X as Function of A,B by A1, FUNCOP_1:57;
take f ; :: thesis: f is non-empty
let n be set ; :: according to FUNCT_1:def 15 :: thesis: ( not n in proj1 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:19;
hence not f . n is empty by FUNCOP_1:13; :: thesis: verum