let n, m be Ordinal; :: thesis: for b being bag of n st m in n holds
b | m is bag of m
let b be bag of n; :: thesis: ( m in n implies b | m is bag of m )
assume m in n ; :: thesis: b | m is bag of m
then A1: m c= n by ORDINAL1:def 2;
dom b = n by PARTFUN1:def 2;
then dom (b | m) = m by A1, RELAT_1:62;
hence b | m is bag of m by PARTFUN1:def 2; :: thesis: verum