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

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