let i, j be set ; :: thesis: for b1, b2 being bag of j
for b1', b2' being bag of i st b1' = b1 | i & b2' = b2 | i holds
( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
let b1, b2 be bag of j; :: thesis: for b1', b2' being bag of i st b1' = b1 | i & b2' = b2 | i holds
( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
let b1', b2' be bag of i; :: thesis: ( b1' = b1 | i & b2' = b2 | i implies ( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' ) )
assume that
A1: b1' = b1 | i and
A2: b2' = b2 | i ; :: thesis: ( (b1 -' b2) | i = b1' -' b2' & (b1 + b2) | i = b1' + b2' )
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;
dom (b1 + b2) = j by PARTFUN1:def 4;
then A5: dom ((b1 + b2) | i) = j /\ i by RELAT_1:90;

A6: now

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

end;

dom (b1 -' b2) = j by PARTFUN1:def 4;
then A8: dom ((b1 -' b2) | i) = j /\ i by RELAT_1:90;

A9: now

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

end;

dom (b1' -' b2') = i by PARTFUN1:def 4
.= j /\ i by A1, A3, PARTFUN1:def 4 ;
hence (b1 -' b2) | i = b1' -' b2' by A8, A9, FUNCT_1:9; :: thesis: (b1 + b2) | i = b1' + b2'
dom (b1' + b2') = i by PARTFUN1:def 4
.= j /\ i by A1, A3, PARTFUN1:def 4 ;
hence (b1 + b2) | i = b1' + b2' by A5, A6, FUNCT_1:9; :: thesis: verum