A0: dom f = dom (Carrier f) by PRALG_1:def 14;
for x being object st x in dom (Carrier f) holds
not (Carrier f) . x is empty

proof

let x be object ; :: thesis: ( x in dom (Carrier f) implies not (Carrier f) . x is empty )
assume A1: x in dom (Carrier f) ; :: thesis: not (Carrier f) . x is empty
then A5: f . x in rng f by A0, FUNCT_1:3;
then reconsider S = f . x as 1-sorted by PRALG_1:def 11;
A6: not S is empty by A5, WAYBEL_3:def 7;
consider R being 1-sorted such that
A2: R = f . x and
A3: (Carrier f) . x = the carrier of R by PRALG_1:def 14, A0, A1;
thus not (Carrier f) . x is empty by A3, A2, A6; :: thesis: verum

end;

hence Carrier f is non-empty ; :: thesis: verum