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