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 object st u in b holds
u in [:X,NAT:]

proof

let u be object ; :: thesis: ( u in b implies u in [:X,NAT:] )
assume A2: u in b ; :: thesis: u in [:X,NAT:]
then consider u1, u2 being object such that
A3: u = [u1,u2] by RELAT_1:def 1;
u1 in dom b by A2, A3, XTUPLE_0:def 12;
then A4: u1 in X ;
u2 in rng b by A2, A3, XTUPLE_0:def 13;
hence u in [:X,NAT:] by A3, A4, ZFMISC_1:def 2; :: thesis: verum

end;

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