let o1, o2 be Ordinal; :: thesis: for a1, b1, c1 being Element of Bags o1
for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
let a1, b1, c1 be Element of Bags o1; :: thesis: for a2, b2, c2 being Element of Bags o2 st c1 = b1 -' a1 & c2 = b2 -' a2 holds
(b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
let a2, b2, c2 be Element of Bags o2; :: thesis: ( c1 = b1 -' a1 & c2 = b2 -' a2 implies (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2 )
assume that
A1: c1 = b1 -' a1 and
A2: c2 = b2 -' a2 ; :: thesis: (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2
reconsider w = (b1 +^ b2) -' (a1 +^ a2) as Element of Bags (o1 +^ o2) by PRE_POLY:def 12;
for o being Ordinal holds
( ( o in o1 implies w . o = c1 . o ) & ( o in (o1 +^ o2) \ o1 implies w . o = c2 . (o -^ o1) ) )

proof

let o be Ordinal; :: thesis: ( ( o in o1 implies w . o = c1 . o ) & ( o in (o1 +^ o2) \ o1 implies w . o = c2 . (o -^ o1) ) )

hereby :: thesis: ( o in (o1 +^ o2) \ o1 implies w . o = c2 . (o -^ o1) )

assume A3: o in o1 ; :: thesis: w . o = c1 . o
thus w . o = ((b1 +^ b2) . o) -' ((a1 +^ a2) . o) by PRE_POLY:def 6
.= (b1 . o) -' ((a1 +^ a2) . o) by A3, Def1
.= (b1 . o) -' (a1 . o) by A3, Def1
.= c1 . o by A1, PRE_POLY:def 6 ; :: thesis: verum

end;

assume A4: o in (o1 +^ o2) \ o1 ; :: thesis: w . o = c2 . (o -^ o1)
thus w . o = ((b1 +^ b2) . o) -' ((a1 +^ a2) . o) by PRE_POLY:def 6
.= (b2 . (o -^ o1)) -' ((a1 +^ a2) . o) by A4, Def1
.= (b2 . (o -^ o1)) -' (a2 . (o -^ o1)) by A4, Def1
.= c2 . (o -^ o1) by A2, PRE_POLY:def 6 ; :: thesis: verum

end;

hence (b1 +^ b2) -' (a1 +^ a2) = c1 +^ c2 by Def1; :: thesis: verum