let k, n be Nat; :: thesis: for b being bag of n holds (0,n) -cut (b bag_extend k) = b
let b be bag of n; :: thesis: (0,n) -cut (b bag_extend k) = b
thus (0,n) -cut (b bag_extend k) = (b bag_extend k) | n by Th3, NAT_1:11
.= b by HILBASIS:def 1 ; :: thesis: verum