let I be set ; :: thesis: for p being Bags I -valued FinSequence
for a, b being bag of I holds
( <*a*> ^ p is partition of b iff ( a divides b & p is partition of b -' a ) )
let p be Bags I -valued FinSequence; :: thesis: for a, b being bag of I holds
( <*a*> ^ p is partition of b iff ( a divides b & p is partition of b -' a ) )
let a, b be bag of I; :: thesis: ( <*a*> ^ p is partition of b iff ( a divides b & p is partition of b -' a ) )
thus ( <*a*> ^ p is partition of b implies ( a divides b & p is partition of b -' a ) ) :: thesis: ( a divides b & p is partition of b -' a implies <*a*> ^ p is partition of b )
proof
assume b = Sum (<*a*> ^ p) ; :: according to BAGORD_2:def 8 :: thesis: ( a divides b & p is partition of b -' a )
then A1: b = a + (Sum p) by Th25;
hence a divides b by PRE_POLY:50; :: thesis: p is partition of b -' a
thus b -' a = Sum p by A1, PRE_POLY:48; :: according to BAGORD_2:def 8 :: thesis: verum
end;
assume Z1: a divides b ; :: thesis: ( not p is partition of b -' a or <*a*> ^ p is partition of b )
assume b -' a = Sum p ; :: according to BAGORD_2:def 8 :: thesis: <*a*> ^ p is partition of b
then ( (Sum p) + a = (b -' a) + a & (b -' a) + a = b ) by Z1, PRE_POLY:47;
hence b = Sum (<*a*> ^ p) by Th25; :: according to BAGORD_2:def 8 :: thesis: verum