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

for x being object st x in dom (Carrier f) holds

not (Carrier f) . x is empty

proof

hence
Carrier f is non-empty
; :: thesis: verum
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;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