let F be Field; :: thesis: for B being non zero bag of the carrier of F
for S1 being non empty finite Subset of F holds
( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )
let B be non zero bag of the carrier of F; :: thesis: for S1 being non empty finite Subset of F holds
( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )
let S1 be non empty finite Subset of F; :: thesis: ( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )

now :: thesis: ( B divides Bag S1 implies ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) )

assume A: B divides Bag S1 ; :: thesis: ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 )
H: Bag S1 = (S1,1) -bag by RING_5:def 1;
reconsider S2 = support B as non empty finite Subset of F by RING_5:24;

now :: thesis: for o being object st o in the carrier of F holds
B . o = ((S2,1) -bag) . o

let o be object ; :: thesis: ( o in the carrier of F implies B . b₁ = ((S2,1) -bag) . b₁ )
assume o in the carrier of F ; :: thesis: B . b₁ = ((S2,1) -bag) . b₁
then reconsider a = o as Element of F ;
set C = (EmptyBag the carrier of F) +* (S2 --> 1);
C: B . a <= (Bag S1) . a by A, PRE_POLY:def 11;

per cases ( a in S2 or not a in S2 ) ;

suppose B: a in S2 ; :: thesis: B . b₁ = ((S2,1) -bag) . b₁

D: now :: thesis: a in S1

assume not a in S1 ; :: thesis: contradiction
then (Bag S1) . a = 0 by H, UPROOTS:6;
then B . a = 0 by A, PRE_POLY:def 11;
hence contradiction by B, PRE_POLY:def 7; :: thesis: verum

end;

a in dom (S2 --> 1) by B;
then E: ((EmptyBag the carrier of F) +* (S2 --> 1)) . a = (S2 --> 1) . a by FUNCT_4:13
.= 1 by B, FUNCOP_1:7 ;
F: (Bag S1) . a = 1 by D, H, UPROOTS:7;
B . a <> 0 by B, PRE_POLY:def 7;
then B . a >= 1 by NAT_1:14;
hence B . o = ((S2,1) -bag) . o by E, F, C, XXREAL_0:1; :: thesis: verum

end;

suppose B: not a in S2 ; :: thesis: B . b₁ = ((S2,1) -bag) . b₁

then not a in dom (S2 --> 1) ;
then ((EmptyBag the carrier of F) +* (S2 --> 1)) . a = (EmptyBag the carrier of F) . a by FUNCT_4:11
.= 0 by PBOOLE:5
.= B . a by B, PRE_POLY:def 7 ;
hence B . o = ((S2,1) -bag) . o ; :: thesis: verum

end;

end;

end;

then B = (S2,1) -bag by PBOOLE:3
.= Bag S2 by RING_5:def 1 ;
hence ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) by A, bagset1; :: thesis: verum

end;

hence ( B divides Bag S1 iff ex S2 being non empty finite Subset of F st
( B = Bag S2 & S2 c= S1 ) ) by bagset1; :: thesis: verum