let i, k be Nat; :: thesis: for X being set
for x being object
for b being bag of X holds b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))
let X be set ; :: thesis: for x being object
for b being bag of X holds b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))
let x be object ; :: thesis: for b being bag of X holds b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))
let b be bag of X; :: thesis: b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k))
set EX = EmptyBag X;
A1: ( dom (b +* (x,(i + k))) = X & X = dom b ) by PARTFUN1:def 2;
A2: ( dom ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) = X & X = dom (EmptyBag X) ) by PARTFUN1:def 2;
for y being object st y in X holds
(b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y

proof

let y be object ; :: thesis: ( y in X implies (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y )
assume A3: y in X ; :: thesis: (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y

per cases ( x = y or x <> y ) ;

suppose A4: x = y ; :: thesis: (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y

((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y = ((b +* (x,i)) . y) + (((EmptyBag X) +* (x,k)) . y) by PRE_POLY:def 5
.= i + (((EmptyBag X) +* (x,k)) . y) by A4, A1, A3, FUNCT_7:31
.= i + k by A4, A2, A3, FUNCT_7:31 ;
hence (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y by A4, A1, A3, FUNCT_7:31; :: thesis: verum

end;

suppose A5: x <> y ; :: thesis: (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y

A6: ((EmptyBag X) +* (x,k)) . y = (EmptyBag X) . y by A5, FUNCT_7:32
.= 0 ;
A7: (b +* (x,i)) . y = b . y by A5, FUNCT_7:32;
((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y = ((b +* (x,i)) . y) + (((EmptyBag X) +* (x,k)) . y) by PRE_POLY:def 5;
hence (b +* (x,(i + k))) . y = ((b +* (x,i)) + ((EmptyBag X) +* (x,k))) . y by A5, FUNCT_7:32, A7, A6; :: thesis: verum

end;

end;

end;

hence b +* (x,(i + k)) = (b +* (x,i)) + ((EmptyBag X) +* (x,k)) by A1, PARTFUN1:def 2; :: thesis: verum