let X be set ; :: thesis: for b being bag of holds b is PartFunc of X,NAT
let b be bag of ; :: 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 :] )
assume A1: u in b ; :: thesis: u in [:X,NAT :]
then consider u1, u2 being set such that
A2: u = [u1,u2] by RELAT_1:def 1;
u1 in dom b by A1, A2, RELAT_1:def 4;
then A3: u1 in X by PARTFUN1:def 4;
A4: u2 in rng b by A1, A2, RELAT_1:def 5;
rng b c= NAT by VALUED_0:def 6;
hence u in [:X,NAT :] by A2, A3, A4, ZFMISC_1:def 2; :: thesis: verum

end;

then b c= [:X,NAT :] by TARSKI:def 3;
hence b is PartFunc of X,NAT ; :: thesis: verum