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

A6: now :: thesis: for x being object st x in j /\ i holds
((b1 + b2) | i) . x = (b19 + b29) . x

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

end;

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

A9: now :: thesis: for x being object st x in j /\ i holds
((b1 -' b2) | i) . x = (b19 -' b29) . x

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

end;

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