let n be Nat; :: thesis: EmptyBag (n + 1) = (EmptyBag n) bag_extend 0

A1: now :: thesis: for x being object st x in Segm (n + 1) holds
(EmptyBag (n + 1)) . x = ((EmptyBag n) bag_extend 0) . x

let x be object ; :: thesis: ( x in Segm (n + 1) implies (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0) . b₁ )
assume x in Segm (n + 1) ; :: thesis: (EmptyBag (n + 1)) . b₁ = ((EmptyBag n) bag_extend 0) . b₁
then A2: x in (Segm n) \/ {n} by AFINSQ_1:2;

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 PBOOLE:5
.= (EmptyBag n) . x by PBOOLE:5
.= (((EmptyBag n) bag_extend 0) | n) . x by Def1
.= ((EmptyBag n) bag_extend 0) . x by A3, FUNCT_1:49 ; :: 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 PBOOLE:5
.= ((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 2;
hence EmptyBag (n + 1) = (EmptyBag n) bag_extend 0 by A1, FUNCT_1:2; :: thesis: verum