let a1, a2 be Element of Bags (o1 +^ o2); :: thesis: ( ( for o being Ordinal holds
( ( o in o1 implies a1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a1 . o = b . (o -^ o1) ) ) ) & ( for o being Ordinal holds
( ( o in o1 implies a2 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a2 . o = b . (o -^ o1) ) ) ) implies a1 = a2 )
assume that
A24: for o being Ordinal holds
( ( o in o1 implies a1 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a1 . o = b . (o -^ o1) ) ) and
A25: for o being Ordinal holds
( ( o in o1 implies a2 . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies a2 . o = b . (o -^ o1) ) ) ; :: thesis: a1 = a2
A26: dom a1 = o1 +^ o2 by PARTFUN1:def 2;
A27: for c being object st c in dom a1 holds
a1 . c = a2 . c

proof

let c be object ; :: thesis: ( c in dom a1 implies a1 . c = a2 . c )
assume A28: c in dom a1 ; :: thesis: a1 . c = a2 . c
reconsider o = c as Ordinal by A26, A28;
A29: o1 c= o1 +^ o2 by ORDINAL3:24;
A30: ((o1 +^ o2) \ o1) \/ o1 = (o1 +^ o2) \/ o1 by XBOOLE_1:39
.= o1 +^ o2 by A29, XBOOLE_1:12 ;

per cases ( o in o1 or o in (o1 +^ o2) \ o1 ) by A26, A28, A30, XBOOLE_0:def 3;

suppose A31: o in o1 ; :: thesis: a1 . c = a2 . c

hence a1 . c = a . o by A24
.= a2 . c by A25, A31 ;
:: thesis: verum

end;

suppose A32: o in (o1 +^ o2) \ o1 ; :: thesis: a1 . c = a2 . c

hence a1 . c = b . (o -^ o1) by A24
.= a2 . c by A25, A32 ;
:: thesis: verum

end;

end;

end;

dom a1 = dom a2 by A26, PARTFUN1:def 2;
hence a1 = a2 by A27; :: thesis: verum