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;

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

.= 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

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

dom (b1 -' b2) = j
by PARTFUN1:def 2;((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;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

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

dom (b19 -' b29) =
i
by PARTFUN1:def 2
((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;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

.= 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