let i, j be set ; :: thesis: for b1, b2 being bag of
for b1', b2' being bag of st b1' = b1 | i & b2' = b2 | i holds
( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
let b1, b2 be bag of ; :: thesis: for b1', b2' being bag of st b1' = b1 | i & b2' = b2 | i holds
( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
let b1', b2' be bag of ; :: thesis: ( b1' = b1 | i & b2' = b2 | i implies ( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' ) )
assume A1: ( b1' = b1 | i & b2' = b2 | i ) ; :: thesis: ( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
dom (b1 -' b2) = j by PARTFUN1:def 4;
then A2: dom ((b1 -' b2) | i) = j /\ i by RELAT_1:90;
dom b1 = j by PARTFUN1:def 4;
then A3: dom (b1 | i) = j /\ i by RELAT_1:90;
dom b2 = j by PARTFUN1:def 4;
then A4: dom (b2 | i) = j /\ i by RELAT_1:90;
A5: dom (b1' -' b2') = i by PARTFUN1:def 4
.= j /\ i by A1, A3, PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in j /\ i implies ((b1 -' b2) | i) . x = (b1' -' b2') . x )
assume A6: x in j /\ i ; :: thesis: ((b1 -' b2) | i) . x = (b1' -' b2') . x
hence ((b1 -' b2) | i) . x = (b1 -' b2) . x by A2, FUNCT_1:70
.= (b1 . x) -' (b2 . x) by POLYNOM1:def 6
.= (b1' . x) -' (b2 . x) by A1, A3, A6, FUNCT_1:70
.= (b1' . x) -' (b2' . x) by A1, A4, A6, FUNCT_1:70
.= (b1' -' b2') . x by POLYNOM1:def 6 ;
:: thesis: verum

end;

hence (b1 -' b2) | i = b1' -' b2' by A2, A5, FUNCT_1:9; :: thesis: (b1 + b2) | i = b1' + b2'
dom (b1 + b2) = j by PARTFUN1:def 4;
then A7: dom ((b1 + b2) | i) = j /\ i by RELAT_1:90;
A8: dom (b1' + b2') = i by PARTFUN1:def 4
.= j /\ i by A1, A3, PARTFUN1:def 4 ;

now

let x be set ; :: thesis: ( x in j /\ i implies ((b1 + b2) | i) . x = (b1' + b2') . x )
assume A9: x in j /\ i ; :: thesis: ((b1 + b2) | i) . x = (b1' + b2') . x
hence ((b1 + b2) | i) . x = (b1 + b2) . x by A7, FUNCT_1:70
.= (b1 . x) + (b2 . x) by POLYNOM1:def 5
.= (b1' . x) + (b2 . x) by A1, A3, A9, FUNCT_1:70
.= (b1' . x) + (b2' . x) by A1, A4, A9, FUNCT_1:70
.= (b1' + b2') . x by POLYNOM1:def 5 ;
:: thesis: verum

end;

hence (b1 + b2) | i = b1' + b2' by A7, A8, FUNCT_1:9; :: thesis: verum