let n, m be Ordinal; :: thesis: for b1, b2 being bag of n st support b1 = {m} holds
( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) )
let b1, b2 be bag of n; :: thesis: ( support b1 = {m} implies ( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) ) )
assume AS: support b1 = {m} ; :: thesis: ( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) )

A: now :: thesis: ( ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) implies b2 divides b1 )

assume ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) ; :: thesis: b2 divides b1

per cases then ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) ;

suppose b2 = EmptyBag n ; :: thesis: b2 divides b1

hence b2 divides b1 by PRE_POLY:59; :: thesis: verum

end;

suppose A2: ( support b2 = {m} & b2 . m <= b1 . m ) ; :: thesis: b2 divides b1

now :: thesis: for k being object st k in n holds
b2 . k <= b1 . k

let k be object ; :: thesis: ( k in n implies b2 . b₁ <= b1 . b₁ )
assume k in n ; :: thesis: b2 . b₁ <= b1 . b₁

per cases ( k = m or k <> m ) ;

suppose k = m ; :: thesis: b2 . b₁ <= b1 . b₁

hence b2 . k <= b1 . k by A2; :: thesis: verum

end;

suppose k <> m ; :: thesis: b2 . b₁ <= b1 . b₁

then A3: not k in {m} by TARSKI:def 1;
then b2 . k = 0 by A2, PRE_POLY:def 7
.= b1 . k by A3, AS, PRE_POLY:def 7 ;
hence b2 . k <= b1 . k ; :: thesis: verum

end;

end;

end;

hence b2 divides b1 by PRE_POLY:46; :: thesis: verum

end;

end;

end;

H: now :: thesis: for l being object st l <> m holds
b1 . l = 0

let l be object ; :: thesis: ( l <> m implies b1 . l = 0 )
assume l <> m ; :: thesis: b1 . l = 0
then not l in support b1 by AS, TARSKI:def 1;
hence b1 . l = 0 by PRE_POLY:def 7; :: thesis: verum

end;

now :: thesis: ( b2 divides b1 & b2 <> EmptyBag n implies ( support b2 = {m} & b2 . m <= b1 . m ) )

assume A4: b2 divides b1 ; :: thesis: ( b2 <> EmptyBag n implies ( support b2 = {m} & b2 . m <= b1 . m ) )
then A5: b2 <=' b1 by PRE_POLY:49;
assume A6: b2 <> EmptyBag n ; :: thesis: ( support b2 = {m} & b2 . m <= b1 . m )
support b2 = {m}

proof

B: now :: thesis: for o being object st o in support b2 holds
o in {m}

let o be object ; :: thesis: ( o in support b2 implies o in {m} )
assume B1: o in support b2 ; :: thesis: o in {m}

now :: thesis: not o <> m

assume o <> m ; :: thesis: contradiction
then b1 . o = 0 by H;
then b2 . o = 0 by A4, PRE_POLY:def 11;
hence contradiction by B1, PRE_POLY:def 7; :: thesis: verum

end;

hence o in {m} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for o being object st o in {m} holds
o in support b2

let o be object ; :: thesis: ( o in {m} implies o in support b2 )
assume o in {m} ; :: thesis: o in support b2
then B2: o = m by TARSKI:def 1;

now :: thesis: not b2 . m = 0

assume B3: b2 . m = 0 ; :: thesis: contradiction

now :: thesis: for u being object st u in n holds
b2 . u = {}

let u be object ; :: thesis: ( u in n implies b2 . b₁ = {} )
assume u in n ; :: thesis: b2 . b₁ = {}

per cases ( u = m or u <> m ) ;

suppose u = m ; :: thesis: b2 . b₁ = {}

hence b2 . u = {} by B3; :: thesis: verum

end;

suppose u <> m ; :: thesis: b2 . b₁ = {}

then b1 . u = 0 by H;
hence b2 . u = {} by A4, PRE_POLY:def 11; :: thesis: verum

end;

end;

end;

hence contradiction by A6, PBOOLE:6; :: thesis: verum

end;

hence o in support b2 by B2, PRE_POLY:def 7; :: thesis: verum

end;

hence support b2 = {m} by B, TARSKI:2; :: thesis: verum

end;

hence ( support b2 = {m} & b2 . m <= b1 . m ) by A5, AS, Th13e; :: thesis: verum

end;

hence ( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) ) by A; :: thesis: verum