let X be set ; :: thesis: for b being bag of X holds b is PartFunc of X,NAT
let b be bag of X; :: thesis: b is PartFunc of X,NAT
for u being set st u in b holds
u in [:X,NAT:]

proof

let u be set ; :: thesis: ( u in b implies u in [:X,NAT:] )
A1: rng b c= NAT by VALUED_0:def 6;
assume A2: u in b ; :: thesis: u in [:X,NAT:]
then consider u1, u2 being set such that
A3: u = [u1,u2] by RELAT_1:def 1;
u1 in dom b by A2, A3, RELAT_1:def 4;
then A4: u1 in X by PARTFUN1:def 4;
u2 in rng b by A2, A3, RELAT_1:def 5;
hence u in [:X,NAT:] by A3, A4, A1, ZFMISC_1:def 2; :: thesis: verum

end;

hence b is PartFunc of X,NAT by TARSKI:def 3; :: thesis: verum