let n be Element of NAT ; :: thesis: EmptyBag (n + 1) = (EmptyBag n) bag_extend 0

A1: now

let x be set ; :: thesis: ( x in n + 1 implies (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0 ) . b₁ )
assume x in n + 1 ; :: thesis: (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0 ) . b₁
then x in succ n by NAT_1:39;
then A2: x in n \/ {n} by ORDINAL1:def 1;

per cases ( x in n or x in {n} ) by A2, XBOOLE_0:def 3;

suppose A3: x in n ; :: thesis: (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0 ) . b₁

thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52
.= (EmptyBag n) . x by PRE_POLY:52
.= (((EmptyBag n) bag_extend 0 ) | n) . x by Def1
.= ((EmptyBag n) bag_extend 0 ) . x by A3, FUNCT_1:72 ; :: thesis: verum

end;

suppose A4: x in {n} ; :: thesis: (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0 ) . b₁

thus (EmptyBag (n + 1)) . x = 0 by PRE_POLY:52
.= ((EmptyBag n) bag_extend 0 ) . n by Def1
.= ((EmptyBag n) bag_extend 0 ) . x by A4, TARSKI:def 1 ; :: thesis: verum

end;

end;

end;

( dom (EmptyBag (n + 1)) = n + 1 & dom ((EmptyBag n) bag_extend 0 ) = n + 1 ) by PARTFUN1:def 4;
hence EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 by A1, FUNCT_1:9; :: thesis: verum