let I, J be set ; :: thesis: for m being bag of I st support m c= J holds
m | J = m
let m be bag of I; :: thesis: ( support m c= J implies m | J = m )
assume A1: support m c= J ; :: thesis: m | J = m
let i be object ; :: according to PBOOLE:def 10 :: thesis: ( not i in I or (m | J) . i = m . i )
assume A2: i in I ; :: thesis: (m | J) . i = m . i
per cases ( i in J or not i in J ) ;
suppose i in J ; :: thesis: (m | J) . i = m . i
hence (m | J) . i = m . i by A2, BAR; :: thesis: verum
end;
suppose not i in J ; :: thesis: (m | J) . i = m . i
then ( (m | J) . i = 0 & not i in support m ) by A1, A2, BAR;
hence (m | J) . i = m . i by PRE_POLY:def 7; :: thesis: verum
end;
end;