let b1, b2 be bag of I; :: thesis: ( ( for i being object st i in I holds
( ( i in J implies b1 . i = m . i ) & ( not i in J implies b1 . i = 0 ) ) ) & ( for i being object st i in I holds
( ( i in J implies b2 . i = m . i ) & ( not i in J implies b2 . i = 0 ) ) ) implies b1 = b2 )
assume that
A1: for i being object st i in I holds
( ( i in J implies b1 . i = m . i ) & ( not i in J implies b1 . i = 0 ) ) and
A2: for i being object st i in I holds
( ( i in J implies b2 . i = m . i ) & ( not i in J implies b2 . i = 0 ) ) ; :: thesis: b1 = b2
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or b1 . i = b2 . i )
assume A3: i in I ; :: thesis: b1 . i = b2 . i
per cases ( i in J or not i in J ) ;
suppose i in J ; :: thesis: b1 . i = b2 . i
then ( b1 . i = m . i & m . i = b2 . i ) by A1, A2, A3;
hence b1 . i = b2 . i ; :: thesis: verum
end;
suppose not i in J ; :: thesis: b1 . i = b2 . i
then ( b1 . i = 0 & 0 = b2 . i ) by A1, A2, A3;
hence b1 . i = b2 . i ; :: thesis: verum
end;
end;