let F be Field; :: thesis: for S1, S2 being non empty finite Subset of F holds
( Bag S1 divides Bag S2 iff S1 c= S2 )
let S1, S2 be non empty finite Subset of F; :: thesis: ( Bag S1 divides Bag S2 iff S1 c= S2 )
H1: ( Bag S1 = (S1,1) -bag & Bag S2 = (S2,1) -bag ) by RING_5:def 1;

A: now :: thesis: ( Bag S1 divides Bag S2 implies S1 c= S2 )

assume B: Bag S1 divides Bag S2 ; :: thesis: S1 c= S2

now :: thesis: for o being object st o in S1 holds
o in S2

let o be object ; :: thesis: ( o in S1 implies o in S2 )
assume o in S1 ; :: thesis: o in S2
then C: 1 = (Bag S1) . o by H1, UPROOTS:7;
(Bag S1) . o <= (Bag S2) . o by B, PRE_POLY:def 11;
hence o in S2 by C, H1, UPROOTS:6; :: thesis: verum

end;

hence S1 c= S2 ; :: thesis: verum

end;

now :: thesis: ( S1 c= S2 implies Bag S1 divides Bag S2 )

assume C: S1 c= S2 ; :: thesis: Bag S1 divides Bag S2

now :: thesis: for o being object holds (Bag S1) . o <= (Bag S2) . o

let o be object ; :: thesis: (Bag S1) . b₁ <= (Bag S2) . b₁

per cases ( o in S1 or not o in S1 ) ;

suppose B: o in S1 ; :: thesis: (Bag S1) . b₁ <= (Bag S2) . b₁

then (Bag S1) . o = 1 by H1, UPROOTS:7
.= (Bag S2) . o by C, B, H1, UPROOTS:7 ;
hence (Bag S1) . o <= (Bag S2) . o ; :: thesis: verum

end;

suppose not o in S1 ; :: thesis: (Bag S1) . b₁ <= (Bag S2) . b₁

hence (Bag S1) . o <= (Bag S2) . o by H1, UPROOTS:6; :: thesis: verum

end;

end;

end;

hence Bag S1 divides Bag S2 by PRE_POLY:def 11; :: thesis: verum

end;

hence ( Bag S1 divides Bag S2 iff S1 c= S2 ) by A; :: thesis: verum