:: INT_7 semantic presentation

begin

   Lm1:  for x, X, y, z being set st z <> x holds
((X --> 0) +* (x,y)) . z = 0
proof
let x, X, y, z be set ; ::_thesis: ( z <> x implies ((X --> 0) +* (x,y)) . z = 0 )
assume A1: z <> x ; ::_thesis: ((X --> 0) +* (x,y)) . z = 0
A2: dom (X --> 0) = X by FUNCOP_1:13;
percases ( z in X or not z in X ) ;
supposeA3: z in X ; ::_thesis: ((X --> 0) +* (x,y)) . z = 0
((X --> 0) +* (x,y)) . z = (X --> 0) . z by A1, FUNCT_7:32
.= 0 by A3, FUNCOP_1:7 ;
hence  ((X --> 0) +* (x,y)) . z = 0 ; ::_thesis: verum
end;
supposeA4: not z in X ; ::_thesis: ((X --> 0) +* (x,y)) . z = 0
((X --> 0) +* (x,y)) . z = (X --> 0) . z by A1, FUNCT_7:32
.= 0 by A2, A4, FUNCT_1:def_2 ;
hence  ((X --> 0) +* (x,y)) . z = 0 ; ::_thesis: verum
end;
end;
end;

theorem Th1: :: INT_7:1
for X, x being set
for p being ManySortedSet of X st support p = {x} holds
p = (X --> 0) +* (x,(p . x))
proof
let X, x be set ; ::_thesis: for p being ManySortedSet of X st support p = {x} holds
p = (X --> 0) +* (x,(p . x))
let p be ManySortedSet of X; ::_thesis: ( support p = {x} implies p = (X --> 0) +* (x,(p . x)) )
assume A1: support p = {x} ; ::_thesis: p = (X --> 0) +* (x,(p . x))
A2: for y being set st y in dom p holds
p . y = ((X --> 0) +* (x,(p . x))) . y
proof
let y be set ; ::_thesis: ( y in dom p implies p . y = ((X --> 0) +* (x,(p . x))) . y )
assume  y in dom p ; ::_thesis: p . y = ((X --> 0) +* (x,(p . x))) . y
then  y in X ;
then A3: y in dom (X --> 0) by FUNCOP_1:13;
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: p . y = ((X --> 0) +* (x,(p . x))) . y
hence  p . y = ((X --> 0) +* (x,(p . x))) . y by A3, FUNCT_7:31; ::_thesis: verum
end;
supposeA4: x <> y ; ::_thesis: p . y = ((X --> 0) +* (x,(p . x))) . y
then  not y in support p by A1, TARSKI:def_1;
then  p . y = 0 by PRE_POLY:def_7;
hence  p . y = ((X --> 0) +* (x,(p . x))) . y by A4, Lm1; ::_thesis: verum
end;
end;
end;
dom ((X --> 0) +* (x,(p . x))) = dom (X --> 0) by FUNCT_7:30
.= X by FUNCOP_1:13 ;
then  dom p = dom ((X --> 0) +* (x,(p . x))) by PARTFUN1:def_2;
hence  p = (X --> 0) +* (x,(p . x)) by A2, FUNCT_1:2; ::_thesis: verum
end;

theorem Th2: :: INT_7:2
for X being set
for p, q, r being real-valued ManySortedSet of X st (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) holds
p + q = r
proof
let X be set ; ::_thesis: for p, q, r being real-valued ManySortedSet of X st (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) holds
p + q = r
let p, q, r be real-valued ManySortedSet of X; ::_thesis: ( (support p) /\ (support q) = {} & (support p) \/ (support q) = support r & p | (support p) = r | (support p) & q | (support q) = r | (support q) implies p + q = r )
assume that
A1: (support p) /\ (support q) = {} and
A2: (support p) \/ (support q) = support r and
A3: p | (support p) = r | (support p) and
A4: q | (support q) = r | (support q) ; ::_thesis: p + q = r
 for x being set st x in X holds
r . x = (p . x) + (q . x)
proof
let x be set ; ::_thesis: ( x in X implies r . x = (p . x) + (q . x) )
assume  x in X ; ::_thesis: r . x = (p . x) + (q . x)
percases ( x in (support p) \/ (support q) or not x in (support p) \/ (support q) ) ;
supposeA5: x in (support p) \/ (support q) ; ::_thesis: r . x = (p . x) + (q . x)
now__::_thesis:_r_._x_=_(p_._x)_+_(q_._x)
percases ( x in support p or x in support q ) by A5, XBOOLE_0:def_3;
supposeA6: x in support p ; ::_thesis: r . x = (p . x) + (q . x)
then A7: not x in support q by A1, XBOOLE_0:def_4;
thus r . x = (r | (support p)) . x by A6, FUNCT_1:49
.= (p . x) + 0 by A3, A6, FUNCT_1:49
.= (p . x) + (q . x) by A7, PRE_POLY:def_7 ; ::_thesis: verum
end;
supposeA8: x in support q ; ::_thesis: r . x = (p . x) + (q . x)
then A9: not x in support p by A1, XBOOLE_0:def_4;
thus r . x = (r | (support q)) . x by A8, FUNCT_1:49
.= 0 + (q . x) by A4, A8, FUNCT_1:49
.= (p . x) + (q . x) by A9, PRE_POLY:def_7 ; ::_thesis: verum
end;
end;
end;
hence  r . x = (p . x) + (q . x) ; ::_thesis: verum
end;
supposeA10: not x in (support p) \/ (support q) ; ::_thesis: r . x = (p . x) + (q . x)
then A11: not x in support q by XBOOLE_0:def_3;
A12: not x in support p by A10, XBOOLE_0:def_3;
thus r . x = 0 by A2, A10, PRE_POLY:def_7
.= 0 + (q . x) by A11, PRE_POLY:def_7
.= (p . x) + (q . x) by A12, PRE_POLY:def_7 ; ::_thesis: verum
end;
end;
end;
hence  r = p + q by PRE_POLY:33; ::_thesis: verum
end;

theorem Th3: :: INT_7:3
for X being set
for p, q being ManySortedSet of X st p | (support p) = q | (support q) holds
p = q
proof
let X be set ; ::_thesis: for p, q being ManySortedSet of X st p | (support p) = q | (support q) holds
p = q
let p, q be ManySortedSet of X; ::_thesis: ( p | (support p) = q | (support q) implies p = q )
A1: dom (p | (support p)) = (dom p) /\ (support p) by RELAT_1:61
.= support p by PRE_POLY:37, XBOOLE_1:28 ;
A2: dom (q | (support q)) = (dom q) /\ (support q) by RELAT_1:61
.= support q by PRE_POLY:37, XBOOLE_1:28 ;
assume A3: p | (support p) = q | (support q) ; ::_thesis: p = q
A4: for x being set st x in X holds
p . x = q . x
proof
let x be set ; ::_thesis: ( x in X implies p . x = q . x )
assume  x in X ; ::_thesis: p . x = q . x
percases ( x in support p or not x in support p ) ;
supposeA5: x in support p ; ::_thesis: p . x = q . x
hence p . x = (p | (support p)) . x by FUNCT_1:49
.= q . x by A3, A1, A2, A5, FUNCT_1:49 ;
::_thesis: verum
end;
supposeA6: not x in support p ; ::_thesis: p . x = q . x
hence p . x = 0 by PRE_POLY:def_7
.= q . x by A3, A1, A2, A6, PRE_POLY:def_7 ;
::_thesis: verum
end;
end;
end;
A7: dom q = X by PARTFUN1:def_2;
 dom p = X by PARTFUN1:def_2;
hence  p = q by A4, A7, FUNCT_1:2; ::_thesis: verum
end;

theorem Th4: :: INT_7:4
for X being set
for p, q being bag of X st support p = {} & support q = {} holds
p = q
proof
let X be set ; ::_thesis: for p, q being bag of X st support p = {} & support q = {} holds
p = q
let p, q be bag of X; ::_thesis: ( support p = {} & support q = {} implies p = q )
assume that
A1: support p = {} and
A2: support q = {} ; ::_thesis: p = q
A3: {} = (dom q) /\ {}
.= dom (q | (support q)) by A2 ;
A4: dom (p | (support p)) = (dom p) /\ (support p) by RELAT_1:61
.= {} by A1 ;
then  for x being set st x in dom (p | (support p)) holds
(p | (support p)) . x = (q | (support q)) . x ;
hence  p = q by A4, A3, Th3, FUNCT_1:2; ::_thesis: verum
end;

Lm2:  for p, q being bag of SetPrimes st support p c= support q & p | (support p) = q | (support p) holds
ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )
proof
deffunc H1( set ) ->  Element of NAT = 0 ;
let p, q be bag of SetPrimes ; ::_thesis: ( support p c= support q & p | (support p) = q | (support p) implies ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) )
assume that
A1: support p c= support q and
A2: p | (support p) = q | (support p) ; ::_thesis: ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )
deffunc H2( set ) ->  Element of NAT = q . $1;
defpred S1[ set ] means $1 in (support q) \ (support p);
A3: for x being set st x in SetPrimes holds
( ( S1[x] implies H2(x) in NAT ) & ( not S1[x] implies H1(x) in NAT ) ) ;
consider f being Function of SetPrimes,NAT such that
A4: for x being set st x in SetPrimes holds
( ( S1[x] implies f . x = H2(x) ) & ( not S1[x] implies f . x = H1(x) ) ) from FUNCT_2:sch_5(A3);
A5: for x being set st x in SetPrimes & x in (support q) \ (support p) holds
f . x <> 0
proof
let x be set ; ::_thesis: ( x in SetPrimes & x in (support q) \ (support p) implies f . x <> 0 )
assume that
 x in SetPrimes and
A6: x in (support q) \ (support p) ; ::_thesis: f . x <> 0
 x in support q by A6, XBOOLE_0:def_5;
then  q . x <> 0 by PRE_POLY:def_7;
hence  f . x <> 0 by A4, A6; ::_thesis: verum
end;
A7: for x being set st not x in SetPrimes holds
f . x = 0
proof
let x be set ; ::_thesis: ( not x in SetPrimes implies f . x = 0 )
assume  not x in SetPrimes ; ::_thesis: f . x = 0
then  not x in dom f ;
hence  f . x = 0 by FUNCT_1:def_2; ::_thesis: verum
end;
A8: for x being set holds
( x in (support q) \ (support p) iff f . x <> 0 )
proof
let x be set ; ::_thesis: ( x in (support q) \ (support p) iff f . x <> 0 )
percases ( x in SetPrimes or not x in SetPrimes ) ;
suppose x in SetPrimes ; ::_thesis: ( x in (support q) \ (support p) iff f . x <> 0 )
hence  ( x in (support q) \ (support p) iff f . x <> 0 ) by A4, A5; ::_thesis: verum
end;
suppose not x in SetPrimes ; ::_thesis: ( x in (support q) \ (support p) iff f . x <> 0 )
hence  ( x in (support q) \ (support p) iff f . x <> 0 ) by A7; ::_thesis: verum
end;
end;
end;
then  support f is finite by PRE_POLY:def_7;
then reconsider r = f as bag of SetPrimes by PRE_POLY:def_8;
A9: (support p) \/ (support r) = (support p) \/ ((support q) \ (support p)) by A8, PRE_POLY:def_7
.= (support p) \/ (support q) by XBOOLE_1:39
.= support q by A1, XBOOLE_1:12 ;
A10: dom (f | (support f)) = (dom f) /\ (support f) by RELAT_1:61
.= support f by PRE_POLY:37, XBOOLE_1:28 ;
A11: support f = (support q) \ (support p) by A8, PRE_POLY:def_7;
A12: for x being set st x in dom (f | (support f)) holds
(f | (support f)) . x = (q | (support f)) . x
proof
let x be set ; ::_thesis: ( x in dom (f | (support f)) implies (f | (support f)) . x = (q | (support f)) . x )
assume A13: x in dom (f | (support f)) ; ::_thesis: (f | (support f)) . x = (q | (support f)) . x
then A14: (q | (support f)) . x = q . x by A10, FUNCT_1:49;
 (f | (support f)) . x = f . x by A10, A13, FUNCT_1:49;
hence  (f | (support f)) . x = (q | (support f)) . x by A4, A11, A10, A13, A14; ::_thesis: verum
end;
dom (q | (support f)) = (dom q) /\ (support f) by RELAT_1:61
.= (dom q) /\ ((support q) \ (support p)) by A8, PRE_POLY:def_7
.= ((dom q) /\ (support q)) \ (support p) by XBOOLE_1:49
.= (support q) \ (support p) by PRE_POLY:37, XBOOLE_1:28
.= support f by A8, PRE_POLY:def_7 ;
then A15: f | (support f) = q | (support f) by A10, A12, FUNCT_1:def_11;
A16: support p misses support f
proof
assume  support p meets support f ; ::_thesis: contradiction
then  ex x being set st
( x in support p & x in support f ) by XBOOLE_0:3;
hence  contradiction by A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then  (support p) /\ (support f) = {} by XBOOLE_0:def_7;
then  p + r = q by A2, A15, A9, Th2;
hence  ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q ) by A11, A16, A15; ::_thesis: verum
end;

Lm3:  for p being bag of SetPrimes
for X being set st X c= support p holds
ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
proof
let p be bag of SetPrimes ; ::_thesis: for X being set st X c= support p holds
ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
let X be set ; ::_thesis: ( X c= support p implies ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p ) )
set fq = p +* (X --> 0);
A1: rng (p +* (X --> 0)) c= (rng p) \/ (rng (X --> 0)) by FUNCT_4:17;
A2: rng (X --> 0) c= NAT by RELAT_1:def_19;
A3: rng p c= NAT by VALUED_0:def_6;
then  (rng p) \/ (rng (X --> 0)) c= NAT by A2, XBOOLE_1:8;
then A4: rng (p +* (X --> 0)) c= NAT by A1, XBOOLE_1:1;
set fr = p +* ((SetPrimes \ X) --> 0);
A5: dom (p +* ((SetPrimes \ X) --> 0)) = (dom p) \/ (dom ((SetPrimes \ X) --> 0)) by FUNCT_4:def_1
.= (dom p) \/ (SetPrimes \ X) by FUNCOP_1:13
.= SetPrimes \/ (SetPrimes \ X) by PARTFUN1:def_2
.= SetPrimes by XBOOLE_1:12, XBOOLE_1:36 ;
A6: rng (p +* ((SetPrimes \ X) --> 0)) c= (rng p) \/ (rng ((SetPrimes \ X) --> 0)) by FUNCT_4:17;
 rng ((SetPrimes \ X) --> 0) c= NAT by RELAT_1:def_19;
then  (rng p) \/ (rng ((SetPrimes \ X) --> 0)) c= NAT by A3, XBOOLE_1:8;
then  rng (p +* ((SetPrimes \ X) --> 0)) c= NAT by A6, XBOOLE_1:1;
then reconsider fr = p +* ((SetPrimes \ X) --> 0) as Function of SetPrimes,NAT by A5, FUNCT_2:def_1, RELSET_1:4;
assume A7: X c= support p ; ::_thesis: ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
A8: for x being set st not x in X & x in SetPrimes holds
fr . x = 0
proof
let x be set ; ::_thesis: ( not x in X & x in SetPrimes implies fr . x = 0 )
assume that
A9: not x in X and
A10: x in SetPrimes ; ::_thesis: fr . x = 0
A11: x in SetPrimes \ X by A9, A10, XBOOLE_0:def_5;
then  x in dom ((SetPrimes \ X) --> 0) by FUNCOP_1:13;
then  fr . x = ((SetPrimes \ X) --> 0) . x by FUNCT_4:13;
hence  fr . x = 0 by A11, FUNCOP_1:7; ::_thesis: verum
end;
A12: dom (X --> 0) = X by FUNCOP_1:13;
then  dom (p +* (X --> 0)) = (dom p) \/ X by FUNCT_4:def_1
.= SetPrimes \/ X by PARTFUN1:def_2
.= SetPrimes by A7, XBOOLE_1:1, XBOOLE_1:12 ;
then reconsider fq = p +* (X --> 0) as Function of SetPrimes,NAT by A4, FUNCT_2:def_1, RELSET_1:4;
A13: dom (fq | (support fq)) = (dom fq) /\ (support fq) by RELAT_1:61
.= support fq by PRE_POLY:37, XBOOLE_1:28 ;
A14: for x being set st not x in SetPrimes holds
( fr . x = 0 & fq . x = 0 )
proof
let x be set ; ::_thesis: ( not x in SetPrimes implies ( fr . x = 0 & fq . x = 0 ) )
assume A15: not x in SetPrimes ; ::_thesis: ( fr . x = 0 & fq . x = 0 )
then A16: not x in dom fr ;
 not x in dom fq by A15;
hence  ( fr . x = 0 & fq . x = 0 ) by A16, FUNCT_1:def_2; ::_thesis: verum
end;
A17: for x being set st x in X holds
fr . x = p . x
proof
let x be set ; ::_thesis: ( x in X implies fr . x = p . x )
assume  x in X ; ::_thesis: fr . x = p . x
then  not x in dom ((SetPrimes \ X) --> 0) by XBOOLE_0:def_5;
hence  fr . x = p . x by FUNCT_4:11; ::_thesis: verum
end;
A18: for x being set st x in SetPrimes & x in X holds
fr . x <> 0
proof
let x be set ; ::_thesis: ( x in SetPrimes & x in X implies fr . x <> 0 )
assume that
 x in SetPrimes and
A19: x in X ; ::_thesis: fr . x <> 0
 p . x <> 0 by A7, A19, PRE_POLY:def_7;
hence  fr . x <> 0 by A17, A19; ::_thesis: verum
end;
A20: for x being set holds
( x in X iff fr . x <> 0 )
proof
let x be set ; ::_thesis: ( x in X iff fr . x <> 0 )
now__::_thesis:_(_x_in_X_iff_fr_._x_<>_0_)
percases ( x in SetPrimes or not x in SetPrimes ) ;
suppose x in SetPrimes ; ::_thesis: ( x in X iff fr . x <> 0 )
hence  ( x in X iff fr . x <> 0 ) by A8, A18; ::_thesis: verum
end;
supposeA21: not x in SetPrimes ; ::_thesis: ( x in X iff fr . x <> 0 )
 X c= SetPrimes by A7, XBOOLE_1:1;
hence  ( x in X iff fr . x <> 0 ) by A14, A21; ::_thesis: verum
end;
end;
end;
hence  ( x in X iff fr . x <> 0 ) ; ::_thesis: verum
end;
then A22: support fr = X by PRE_POLY:def_7;
then reconsider r = fr as bag of SetPrimes by A7, PRE_POLY:def_8;
A23: support p c= dom p by PRE_POLY:37;
A24: dom (fr | (support fr)) = (dom fr) /\ (support fr) by RELAT_1:61
.= support fr by PRE_POLY:37, XBOOLE_1:28
.= X by A20, PRE_POLY:def_7 ;
A25: for x being set st x in dom (fr | (support fr)) holds
(fr | (support fr)) . x = (p | (support fr)) . x
proof
let x be set ; ::_thesis: ( x in dom (fr | (support fr)) implies (fr | (support fr)) . x = (p | (support fr)) . x )
assume A26: x in dom (fr | (support fr)) ; ::_thesis: (fr | (support fr)) . x = (p | (support fr)) . x
then A27: (p | (support fr)) . x = p . x by A22, A24, FUNCT_1:49;
 (fr | (support fr)) . x = fr . x by A22, A24, A26, FUNCT_1:49;
hence  (fr | (support fr)) . x = (p | (support fr)) . x by A17, A24, A26, A27; ::_thesis: verum
end;
dom (p | (support fr)) = (dom p) /\ (support fr) by RELAT_1:61
.= (dom p) /\ X by A20, PRE_POLY:def_7
.= X by A7, A23, XBOOLE_1:1, XBOOLE_1:28 ;
then A28: fr | (support fr) = p | (support fr) by A24, A25, FUNCT_1:def_11;
A29: for x being set st x in X holds
fq . x = 0
proof
let x be set ; ::_thesis: ( x in X implies fq . x = 0 )
assume A30: x in X ; ::_thesis: fq . x = 0
hence fq . x = (X --> 0) . x by A12, FUNCT_4:13
.= 0 by A30, FUNCOP_1:7 ;
::_thesis: verum
end;
A31: for x being set holds
( x in (support p) \ X iff fq . x <> 0 )
proof
let x be set ; ::_thesis: ( x in (support p) \ X iff fq . x <> 0 )
percases ( x in X or not x in X ) ;
suppose x in X ; ::_thesis: ( x in (support p) \ X iff fq . x <> 0 )
hence  ( x in (support p) \ X iff fq . x <> 0 ) by A29, XBOOLE_0:def_5; ::_thesis: verum
end;
supposeA32: not x in X ; ::_thesis: ( x in (support p) \ X iff fq . x <> 0 )
then A33: fq . x = p . x by A12, FUNCT_4:11;
percases ( x in support p or not x in support p ) ;
suppose x in support p ; ::_thesis: ( x in (support p) \ X iff fq . x <> 0 )
hence  ( x in (support p) \ X iff fq . x <> 0 ) by A32, A33, PRE_POLY:def_7, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose not x in support p ; ::_thesis: ( x in (support p) \ X iff fq . x <> 0 )
hence  ( x in (support p) \ X iff fq . x <> 0 ) by A33, PRE_POLY:def_7, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
end;
end;
then A34: support fq = (support p) \ X by PRE_POLY:def_7;
then reconsider q = fq as bag of SetPrimes by PRE_POLY:def_8;
A35: dom (p | (support fq)) = (dom p) /\ (support fq) by RELAT_1:61
.= (dom p) /\ ((support p) \ X) by A31, PRE_POLY:def_7
.= ((dom p) /\ (support p)) \ X by XBOOLE_1:49
.= (support p) \ X by PRE_POLY:37, XBOOLE_1:28
.= support fq by A31, PRE_POLY:def_7 ;
 (support p) \ X misses X by XBOOLE_1:79;
then A36: (support fq) /\ (support fr) = {} by A22, A34, XBOOLE_0:def_7;
A37: for x being set st x in SetPrimes & x in support fq holds
p . x = fq . x
proof
let x be set ; ::_thesis: ( x in SetPrimes & x in support fq implies p . x = fq . x )
assume that
 x in SetPrimes and
A38: x in support fq ; ::_thesis: p . x = fq . x
 not x in X by A22, A36, A38, XBOOLE_0:def_4;
hence  p . x = fq . x by A12, FUNCT_4:11; ::_thesis: verum
end;
 for x being set st x in dom (fq | (support fq)) holds
(fq | (support fq)) . x = (p | (support fq)) . x
proof
let x be set ; ::_thesis: ( x in dom (fq | (support fq)) implies (fq | (support fq)) . x = (p | (support fq)) . x )
assume A39: x in dom (fq | (support fq)) ; ::_thesis: (fq | (support fq)) . x = (p | (support fq)) . x
then A40: (p | (support fq)) . x = p . x by A13, FUNCT_1:49;
 (fq | (support fq)) . x = fq . x by A13, A39, FUNCT_1:49;
hence  (fq | (support fq)) . x = (p | (support fq)) . x by A13, A37, A39, A40; ::_thesis: verum
end;
then A41: fq | (support fq) = p | (support fq) by A13, A35, FUNCT_1:def_11;
(support fr) \/ (support fq) = (support fr) \/ ((support p) \ (support fr)) by A20, A34, PRE_POLY:def_7
.= (support fr) \/ (support p) by XBOOLE_1:39
.= support p by A7, A22, XBOOLE_1:12 ;
then  q + r = p by A36, A41, A28, Th2;
hence  ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p ) by A22, A34, A41, A28, XBOOLE_1:79; ::_thesis: verum
end;

definition
let p be bag of SetPrimes ;
attrp is prime-factorization-like  means :Def1: :: INT_7:def 1
 for x being Prime st x in support p holds
ex n being Nat st
( 0 < n & p . x = x |^ n );
end;

:: deftheorem Def1 defines prime-factorization-like INT_7:def_1_:_
 for p being bag of SetPrimes holds
( p is prime-factorization-like iff for x being Prime st x in support p holds
ex n being Nat st
( 0 < n & p . x = x |^ n ) );

registration
let n be non empty Nat;
cluster prime_factorization n ->  prime-factorization-like ;
coherence
 ppf n is prime-factorization-like
proof
let p be Prime; :: according to INT_7:def_1 ::_thesis: ( p in support (ppf n) implies ex n being Nat st
( 0 < n & (ppf n) . p = p |^ n ) )
assume A1: p in support (ppf n) ; ::_thesis: ex n being Nat st
( 0 < n & (ppf n) . p = p |^ n )
A2: p |-count n <> 0
proof
assume  p |-count n = 0 ; ::_thesis: contradiction
then  (ppf n) . p = 0 by NAT_3:55;
hence  contradiction by A1, PRE_POLY:def_7; ::_thesis: verum
end;
take  p |-count n ; ::_thesis: ( 0 < p |-count n & (ppf n) . p = p |^ (p |-count n) )
 p in support (pfexp n) by A1, NAT_3:def_9;
hence  ( 0 < p |-count n & (ppf n) . p = p |^ (p |-count n) ) by A2, NAT_3:def_9; ::_thesis: verum
end;
end;

theorem Th5: :: INT_7:5
for p, q being Prime
for n, m being Nat st p divides m * (q |^ n) & p <> q holds
p divides m
proof
let p, q be Prime; ::_thesis: for n, m being Nat st p divides m * (q |^ n) & p <> q holds
p divides m
let n, m be Nat; ::_thesis: ( p divides m * (q |^ n) & p <> q implies p divides m )
assume that
A1: p divides m * (q |^ n) and
A2: p <> q ; ::_thesis: p divides m
 ( p divides m or p divides q |^ n ) by A1, NEWTON:80;
hence  p divides m by A2, NAT_3:6; ::_thesis: verum
end;

Lm4:  for a being Prime
for b being bag of SetPrimes st b is prime-factorization-like & a in support b holds
( a divides Product b & ex n being Nat st a |^ n divides Product b )
proof
let a be Prime; ::_thesis: for b being bag of SetPrimes st b is prime-factorization-like & a in support b holds
( a divides Product b & ex n being Nat st a |^ n divides Product b )
let b be bag of SetPrimes ; ::_thesis: ( b is prime-factorization-like & a in support b implies ( a divides Product b & ex n being Nat st a |^ n divides Product b ) )
assume that
A1: b is prime-factorization-like and
A2: a in support b ; ::_thesis: ( a divides Product b & ex n being Nat st a |^ n divides Product b )
consider n being Nat such that
A3: 0 < n and
A4: b . a = a |^ n by A1, A2, Def1;
A5: a divides b . a by A3, A4, NAT_3:3;
A6: rng b c= NAT by VALUED_0:def_6;
 a in rng (canFS (support b)) by A2, FUNCT_2:def_3;
then consider d being set  such that
A7: d in dom (canFS (support b)) and
A8: a = (canFS (support b)) . d by FUNCT_1:def_3;
consider f being FinSequence of COMPLEX  such that
A9: Product b = Product f and
A10: f = b * (canFS (support b)) by NAT_3:def_5;
 rng f c= rng b by A10, RELAT_1:26;
then  rng f c= NAT by A6, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
A11: rng (canFS (support b)) = support b by FUNCT_2:def_3;
 support b c= dom b by PRE_POLY:37;
then A12: dom f = dom (canFS (support b)) by A10, A11, RELAT_1:27;
then  b . a = (b * (canFS (support b))) . d by A10, A7, A8, FUNCT_1:12;
then  b . a in rng f by A10, A12, A7, FUNCT_1:3;
then  a |^ n divides Product f by A4, NAT_3:7;
hence  ( a divides Product b & ex n being Nat st a |^ n divides Product b ) by A9, A4, A5, NAT_D:4; ::_thesis: verum
end;

Lm5:  for p being FinSequence of NAT
for x being Element of NAT
for b being bag of SetPrimes st b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) holds
ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
proof
deffunc H1( set ) ->  Element of NAT = 0 ;
let p be FinSequence of NAT ; ::_thesis: for x being Element of NAT
for b being bag of SetPrimes st b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) holds
ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
let x be Element of NAT ; ::_thesis: for b being bag of SetPrimes st b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) holds
ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
let b be bag of SetPrimes ; ::_thesis: ( b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) implies ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) ) )
assume that
A1: b is prime-factorization-like and
A2: p ^ <*x*> = b * (canFS (support b)) ; ::_thesis: ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
A3: rng (canFS (support b)) = support b by FUNCT_2:def_3;
 dom b = SetPrimes by PARTFUN1:def_2;
then A4: dom (b * (canFS (support b))) = dom (canFS (support b)) by A3, RELAT_1:27;
 p = (b * (canFS (support b))) | (dom p) by A2, FINSEQ_1:21;
then  dom p = (dom (b * (canFS (support b)))) /\ (dom p) by RELAT_1:61;
then A5: dom ((canFS (support b)) | (dom p)) = dom p by A4, RELAT_1:62, XBOOLE_1:17;
deffunc H2( set ) ->  Element of NAT = b . $1;
A6: card (support b) = len (canFS (support b)) by UPROOTS:3;
 dom b = SetPrimes by PARTFUN1:def_2;
then A7: dom (b * (canFS (support b))) = dom (canFS (support b)) by A3, RELAT_1:27;
A8: (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;
A9: len <*x*> = 1 by FINSEQ_1:40;
then  len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:22;
then A10: (len p) + 1 in dom (b * (canFS (support b))) by A2, A8, FINSEQ_1:def_3;
A11: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42
.= b . ((canFS (support b)) . ((len p) + 1)) by A2, A7, A10, FUNCT_1:13 ;
A12: rng (canFS (support b)) = support b by FUNCT_2:def_3;
then A13: (canFS (support b)) . ((len p) + 1) in support b by A7, A10, FUNCT_1:3;
then reconsider q = (canFS (support b)) . ((len p) + 1) as Prime by NEWTON:def_6;
defpred S1[ set ] means $1 in (support b) \ {q};
consider b1 being ManySortedSet of SetPrimes  such that
A14: for i being Element of SetPrimes st i in SetPrimes holds
( ( S1[i] implies b1 . i = H2(i) ) & ( not S1[i] implies b1 . i = H1(i) ) ) from PRE_CIRC:sch_2();
A15: rng b1 c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng b1 or y in NAT )
assume  y in rng b1 ; ::_thesis: y in NAT
then consider x being set  such that
A16: x in dom b1 and
A17: y = b1 . x by FUNCT_1:def_3;
reconsider x = x as Element of SetPrimes by A16;
 b1 . x in NAT
proof
percases ( x in (support b) \ {q} or not x in (support b) \ {q} ) ;
suppose x in (support b) \ {q} ; ::_thesis: b1 . x in NAT
then  b1 . x = b . x by A14;
hence  b1 . x in NAT ; ::_thesis: verum
end;
suppose not x in (support b) \ {q} ; ::_thesis: b1 . x in NAT
then  b1 . x = 0 by A14;
hence  b1 . x in NAT ; ::_thesis: verum
end;
end;
end;
hence  y in NAT by A17; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_support_b1_holds_
z_in_(support_b)_\_{q}
let z be set ; ::_thesis: ( z in support b1 implies z in (support b) \ {q} )
assume A18: z in support b1 ; ::_thesis: z in (support b) \ {q}
 z in dom b1
proof
assume  not z in dom b1 ; ::_thesis: contradiction
then  b1 . z = {} by FUNCT_1:def_2;
hence  contradiction by A18, PRE_POLY:def_7; ::_thesis: verum
end;
then reconsider y = z as Element of SetPrimes ;
assume A19: not z in (support b) \ {q} ; ::_thesis: contradiction
 b1 . y <> 0 by A18, PRE_POLY:def_7;
hence  contradiction by A14, A19; ::_thesis: verum
end;
then A20: support b1 c= (support b) \ {q} by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_(support_b)_\_{q}_holds_
z_in_support_b1
let z be set ; ::_thesis: ( z in (support b) \ {q} implies z in support b1 )
assume A21: z in (support b) \ {q} ; ::_thesis: z in support b1
then A22: z in support b by XBOOLE_0:def_5;
reconsider y = z as Element of SetPrimes by A21;
 b1 . y = b . y by A14, A21;
then  b1 . y <> 0 by A22, PRE_POLY:def_7;
hence  z in support b1 by PRE_POLY:def_7; ::_thesis: verum
end;
then A23: (support b) \ {q} c= support b1 by TARSKI:def_3;
then A24: support b1 = (support b) \ {q} by A20, XBOOLE_0:def_10;
reconsider b1 = b1 as bag of SetPrimes by A20, A15, PRE_POLY:def_8, VALUED_0:def_6;
consider n being Nat such that
A25: 0 < n and
A26: b . q = q |^ n by A1, A13, Def1;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A27: rng (canFS (support b)) = support b by FUNCT_2:def_3;
 SetPrimes = dom b by PARTFUN1:def_2;
then  card (dom (b * (canFS (support b)))) = card (dom (canFS (support b))) by A27, RELAT_1:27
.= card (Seg (len (canFS (support b)))) by FINSEQ_1:def_3
.= card (len (canFS (support b))) by FINSEQ_1:55
.= len (canFS (support b)) ;
then A28: len (canFS (support b)) = card (Seg (len (p ^ <*x*>))) by A2, FINSEQ_1:def_3
.= card (len (p ^ <*x*>)) by FINSEQ_1:55
.= (len p) + 1 by A9, FINSEQ_1:22 ;
card ((support b) \ {q}) = (card (support b)) - (card {q}) by A7, A12, A10, EULER_1:4, FUNCT_1:3
.= (card (support b)) - 1 by CARD_1:30 ;
then A29: len (canFS (support b1)) = len p by A24, A28, A6, UPROOTS:3;
then A30: dom (canFS (support b1)) = Seg (len p) by FINSEQ_1:def_3;
then A31: dom (canFS (support b1)) = dom p by FINSEQ_1:def_3;
A32: now__::_thesis:_for_x_being_Prime_st_x_in_support_b1_holds_
ex_m_being_Nat_st_
(_0_<_m_&_b1_._x_=_x_|^_m_)
let x be Prime; ::_thesis: ( x in support b1 implies ex m being Nat st
( 0 < m & b1 . x = x |^ m ) )
assume A33: x in support b1 ; ::_thesis: ex m being Nat st
( 0 < m & b1 . x = x |^ m )
 (support b) \ {q} c= support b by XBOOLE_1:36;
then consider m being Nat such that
A34: 0 < m and
A35: b . x = x |^ m by A1, A24, A33, Def1;
take m = m; ::_thesis: ( 0 < m & b1 . x = x |^ m )
thus  0 < m by A34; ::_thesis: b1 . x = x |^ m
thus  b1 . x = x |^ m by A14, A20, A33, A35; ::_thesis: verum
end;
percases ( dom p = {} or dom p <> {} ) ;
supposeA36: dom p = {} ; ::_thesis: ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
set p1 = b1 * (canFS (support b1));
A37: p = {} by A36;
Seg (len (canFS (support b1))) = dom (canFS (support b1)) by FINSEQ_1:def_3
.= Seg (len p) by A29, FINSEQ_1:def_3
.= Seg 0 by A37 ;
then  canFS (support b1) = {} ;
then A38: b1 * (canFS (support b1)) = <*> NAT ;
then reconsider p1 = b1 * (canFS (support b1)) as FinSequence of NAT ;
take  p1 ; ::_thesis: ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  q ; ::_thesis: ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  n ; ::_thesis: ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  b1 ; ::_thesis: ( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
thus  ( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) ) by A7, A12, A10, A11, A25, A26, A20, A23, A32, A36, A38, Def1, FUNCT_1:3, RELAT_1:41, XBOOLE_0:def_10; ::_thesis: verum
end;
supposeA39: dom p <> {} ; ::_thesis: ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
A40: rng (canFS (support b)) = support b by FUNCT_2:def_3;
now__::_thesis:_for_y_being_set_st_y_in_(support_b)_\_{q}_holds_
y_in_rng_((canFS_(support_b))_|_(dom_p))
let y be set ; ::_thesis: ( y in (support b) \ {q} implies y in rng ((canFS (support b)) | (dom p)) )
assume A41: y in (support b) \ {q} ; ::_thesis: y in rng ((canFS (support b)) | (dom p))
then  y in rng (canFS (support b)) by A40, XBOOLE_0:def_5;
then consider x being set  such that
A42: x in dom (canFS (support b)) and
A43: y = (canFS (support b)) . x by FUNCT_1:def_3;
A44: x in dom p
proof
assume  not x in dom p ; ::_thesis: contradiction
then A45: not x in Seg (len p) by FINSEQ_1:def_3;
A46: x in Seg ((len p) + 1) by A28, A42, FINSEQ_1:def_3;
reconsider x = x as Element of NAT by A42;
 1 <= x by A46, FINSEQ_1:1;
then  len p < x by A45;
then A47: (len p) + 1 <= x by NAT_1:13;
 x <= (len p) + 1 by A46, FINSEQ_1:1;
then  x = (len p) + 1 by A47, XXREAL_0:1;
then  y in {q} by A43, TARSKI:def_1;
hence  contradiction by A41, XBOOLE_0:def_5; ::_thesis: verum
end;
then  x in (dom (canFS (support b))) /\ (dom p) by A42, XBOOLE_0:def_4;
then A48: x in dom ((canFS (support b)) | (dom p)) by RELAT_1:61;
 y = ((canFS (support b)) | (dom p)) . x by A43, A44, FUNCT_1:49;
hence  y in rng ((canFS (support b)) | (dom p)) by A48, FUNCT_1:3; ::_thesis: verum
end;
then A49: (support b) \ {q} c= rng ((canFS (support b)) | (dom p)) by TARSKI:def_3;
now__::_thesis:_for_y_being_set_st_y_in_rng_((canFS_(support_b))_|_(dom_p))_holds_
y_in_(support_b)_\_{q}
let y be set ; ::_thesis: ( y in rng ((canFS (support b)) | (dom p)) implies y in (support b) \ {q} )
assume  y in rng ((canFS (support b)) | (dom p)) ; ::_thesis: y in (support b) \ {q}
then consider x being set  such that
A50: x in dom ((canFS (support b)) | (dom p)) and
A51: y = ((canFS (support b)) | (dom p)) . x by FUNCT_1:def_3;
A52: y = (canFS (support b)) . x by A50, A51, FUNCT_1:47;
A53: x in (dom (canFS (support b))) /\ (dom p) by A50, RELAT_1:61;
then A54: x in dom (canFS (support b)) by XBOOLE_0:def_4;
A55: x in dom p by A53, XBOOLE_0:def_4;
 y <> q
proof
 (len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:4;
then A56: (len p) + 1 in dom (canFS (support b)) by A28, FINSEQ_1:def_3;
assume  y = q ; ::_thesis: contradiction
then  (len p) + 1 = x by A52, A54, A56, FUNCT_1:def_4;
then A57: (len p) + 1 in Seg (len p) by A55, FINSEQ_1:def_3;
 (len p) + 0 < 1 + (len p) by XREAL_1:8;
hence  contradiction by A57, FINSEQ_1:1; ::_thesis: verum
end;
then A58: not y in {q} by TARSKI:def_1;
 y in rng (canFS (support b)) by A52, A54, FUNCT_1:3;
hence  y in (support b) \ {q} by A58, XBOOLE_0:def_5; ::_thesis: verum
end;
then  rng ((canFS (support b)) | (dom p)) c= (support b) \ {q} by TARSKI:def_3;
then A59: rng ((canFS (support b)) | (dom p)) = (support b) \ {q} by A49, XBOOLE_0:def_10;
then reconsider L0 = (canFS (support b)) | (dom p) as Function of (dom p),((support b) \ {q}) by A5, FUNCT_2:1;
A60: L0 is one-to-one by FUNCT_1:52;
then A61: dom (L0 ") = (support b) \ {q} by A59, FUNCT_1:33;
A62: (support b) \ {q} <> {} by A20, A30, A39, FINSEQ_1:def_3;
then  dom L0 = dom p by FUNCT_2:def_1;
then A63: rng (L0 ") = dom p by A60, FUNCT_1:33;
then reconsider LL1 = L0 " as Function of ((support b) \ {q}),(dom p) by A61, FUNCT_2:1;
A64: rng (canFS (support b1)) = support b1 by FUNCT_2:def_3;
then  canFS (support b1) is Function of (dom p),((support b) \ {q}) by A24, A31, FUNCT_2:1;
then reconsider L0L = LL1 * (canFS (support b1)) as Function of (dom p),(dom p) by A62, FUNCT_2:13;
A65: L0 is one-to-one by FUNCT_1:52;
 rng L0L = dom p by A23, A61, A63, A64, RELAT_1:28;
then  L0L is onto by FUNCT_2:def_3;
then reconsider LL = L0L as Permutation of (dom p) by A65;
((canFS (support b)) | (dom p)) * LL = (((canFS (support b)) | (dom p)) * LL1) * (canFS (support b1)) by RELAT_1:36
.= (id (support b1)) * (canFS (support b1)) by A24, A62, A59, A65, FUNCT_2:29
.= canFS (support b1) by FUNCT_2:17 ;
then A66: (canFS (support b1)) * (LL ") = ((canFS (support b)) | (dom p)) * (LL * (LL ")) by RELAT_1:36;
reconsider FS = canFS (support b1) as FinSequence ;
reconsider L = LL " as Permutation of (dom p) ;
A67: rng L = dom FS by A31, FUNCT_2:def_3;
then A68: dom (FS * L) = dom L by RELAT_1:27
.= dom p by A39, FUNCT_2:def_1 ;
set p1 = b1 * FS;
A69: rng (canFS (support b1)) = support b1 by FUNCT_2:def_3;
 SetPrimes = dom b1 by PARTFUN1:def_2;
then A70: dom (b1 * FS) = dom p by A31, A69, RELAT_1:27;
then  dom (b1 * FS) = Seg (len p) by FINSEQ_1:def_3;
then A71: b1 * FS is FinSequence by FINSEQ_1:def_2;
A72: rng (FS * L) = rng FS by A67, RELAT_1:28
.= (support b) \ {q} by A24, FUNCT_2:def_3 ;
 SetPrimes = dom b1 by PARTFUN1:def_2;
then A73: dom p = dom (b1 * (FS * L)) by A68, A72, RELAT_1:27;
 rng LL = dom p by FUNCT_2:def_3;
then A74: (canFS (support b1)) * (LL ") = ((canFS (support b)) | (dom p)) * (id (dom p)) by A39, A66, FUNCT_2:29;
now__::_thesis:_for_k_being_set_st_k_in_dom_p_holds_
p_._k_=_(b1_*_(FS_*_L))_._k
let k be set ; ::_thesis: ( k in dom p implies p . k = (b1 * (FS * L)) . k )
A75: dom p c= dom (p ^ <*x*>) by FINSEQ_1:26;
assume A76: k in dom p ; ::_thesis: p . k = (b1 * (FS * L)) . k
then A77: (FS * L) . k in (support b) \ {q} by A68, A72, FUNCT_1:3;
thus p . k = (p ^ <*x*>) . k by A76, FINSEQ_1:def_7
.= b . ((canFS (support b)) . k) by A2, A76, A75, FUNCT_1:12
.= b . (((canFS (support b)) | (dom p)) . k) by A76, FUNCT_1:49
.= b . ((FS * L) . k) by A74, FUNCT_2:17
.= b1 . ((FS * L) . k) by A14, A77
.= (b1 * (FS * L)) . k by A73, A76, FUNCT_1:12 ; ::_thesis: verum
end;
then p = b1 * (FS * L) by A73, FUNCT_1:2
.= (b1 * FS) * L by RELAT_1:36 ;
then A78: p,b1 * FS are_fiberwise_equipotent by A70, CLASSES1:80;
 rng (b1 * FS) c= NAT by VALUED_0:def_6;
then reconsider p1 = b1 * FS as FinSequence of NAT by A71, FINSEQ_1:def_4;
take  p1 ; ::_thesis: ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  q ; ::_thesis: ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  n ; ::_thesis: ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
take  b1 ; ::_thesis: ( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
 Seg (len p1) = dom p by A70, FINSEQ_1:def_3;
hence  ( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) ) by A7, A12, A10, A11, A25, A26, A20, A23, A32, A78, Def1, EULER_2:10, FINSEQ_1:def_3, FUNCT_1:3, XBOOLE_0:def_10; ::_thesis: verum
end;
end;
end;

Lm6:  for i being Element of NAT
for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st len f = i & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
proof
defpred S1[ Element of NAT ] means  for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st len f = $1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b;
A1: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
thus  S1[k + 1] ::_thesis: verum
proof
A3: 1 <= k + 1 by NAT_1:11;
let f be FinSequence of NAT ; ::_thesis: for b being bag of SetPrimes
for a being Prime st len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let b be bag of SetPrimes ; ::_thesis: for a being Prime st len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let a be Prime; ::_thesis: ( len f = k + 1 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) implies a in support b )
assume that
A4: len f = k + 1 and
A5: b is prime-factorization-like and
 Product b <> 1 and
A6: a divides Product b and
A7: Product b = Product f and
A8: f = b * (canFS (support b)) ; ::_thesis: a in support b
reconsider p = f | k as FinSequence of NAT ;
reconsider x = f . (k + 1) as Element of NAT ;
A9: len p = k by A4, FINSEQ_1:59, NAT_1:11;
A10: f = (f | k) ^ <*(f /. (len f))*> by A4, FINSEQ_5:21
.= p ^ <*x*> by A4, A3, FINSEQ_4:15 ;
then consider p1 being FinSequence of NAT , q being Prime, n being Element of NAT , b1 being bag of SetPrimes  such that
 0 < n and
A11: b1 is prime-factorization-like and
A12: q in support b and
A13: support b1 = (support b) \ {q} and
A14: x = q |^ n and
A15: len p1 = len p and
A16: Product p = Product p1 and
A17: p1 = b1 * (canFS (support b1)) by A5, A8, Lm5;
A18: Product f = (Product p1) * x by A10, A16, RVSUM_1:96;
 rng p1 c= COMPLEX by NUMBERS:20, XBOOLE_1:1;
then  p1 is FinSequence of COMPLEX by FINSEQ_1:def_4;
then A19: Product b1 = Product p1 by A17, NAT_3:def_5;
now__::_thesis:_a_in_support_b
percases ( Product p1 = 1 or Product p1 <> 1 ) ;
supposeA20: Product p1 = 1 ; ::_thesis: a in support b
 a <> 1 by INT_2:def_4;
then  ex k being Element of NAT st a = q * k by A6, A7, A14, A18, A20, PEPIN:32;
then A21: q divides a by INT_1:def_3;
 q <> 1 by INT_2:def_4;
hence  a in support b by A12, A21, INT_2:def_4; ::_thesis: verum
end;
supposeA22: Product p1 <> 1 ; ::_thesis: a in support b
percases ( a = q or a <> q ) ;
suppose a = q ; ::_thesis: a in support b
hence  a in support b by A12; ::_thesis: verum
end;
supposeA23: a <> q ; ::_thesis: a in support b
A24: support b1 c= support b by A13, XBOOLE_1:36;
 a in support b1 by A2, A6, A7, A9, A11, A14, A15, A17, A18, A19, A22, A23, Th5;
hence  a in support b by A24; ::_thesis: verum
end;
end;
end;
end;
end;
hence  a in support b ; ::_thesis: verum
end;
end;
A25: S1[ 0 ]
proof
let f be FinSequence of NAT ; ::_thesis: for b being bag of SetPrimes
for a being Prime st len f = 0 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let b be bag of SetPrimes ; ::_thesis: for a being Prime st len f = 0 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let a be Prime; ::_thesis: ( len f = 0 & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) implies a in support b )
assume  len f = 0 ; ::_thesis: ( not b is prime-factorization-like or not Product b <> 1 or not a divides Product b or not Product b = Product f or not f = b * (canFS (support b)) or a in support b )
then  f = <*> NAT ;
hence  ( not b is prime-factorization-like or not Product b <> 1 or not a divides Product b or not Product b = Product f or not f = b * (canFS (support b)) or a in support b ) by RVSUM_1:94; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A25, A1);
hence  for i being Element of NAT
for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st len f = i & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b ; ::_thesis: verum
end;

theorem Th6: :: INT_7:6
for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
proof
let f be FinSequence of NAT ; ::_thesis: for b being bag of SetPrimes
for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let b be bag of SetPrimes ; ::_thesis: for a being Prime st b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
let a be Prime; ::_thesis: ( b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) implies a in support b )
assume that
A1: b is prime-factorization-like and
A2: Product b <> 1 and
A3: a divides Product b and
A4: Product b = Product f and
A5: f = b * (canFS (support b)) ; ::_thesis: a in support b
 len f is Element of NAT ;
hence  a in support b by A1, A2, A3, A4, A5, Lm6; ::_thesis: verum
end;

Lm7:  for a being Prime
for b being bag of SetPrimes st b is prime-factorization-like & a divides Product b holds
a in support b
proof
let a be Prime; ::_thesis: for b being bag of SetPrimes st b is prime-factorization-like & a divides Product b holds
a in support b
let b be bag of SetPrimes ; ::_thesis: ( b is prime-factorization-like & a divides Product b implies a in support b )
assume that
A1: b is prime-factorization-like and
A2: a divides Product b ; ::_thesis: a in support b
percases ( Product b = 1 or Product b <> 1 ) ;
supposeA3: Product b = 1 ; ::_thesis: a in support b
 a <> 1 by INT_2:def_4;
hence  a in support b by A2, A3, WSIERP_1:15; ::_thesis: verum
end;
supposeA4: Product b <> 1 ; ::_thesis: a in support b
A5: rng b c= NAT by VALUED_0:def_6;
consider f being FinSequence of COMPLEX  such that
A6: Product b = Product f and
A7: f = b * (canFS (support b)) by NAT_3:def_5;
 rng f c= rng b by A7, RELAT_1:26;
then  rng f c= NAT by A5, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
 Product b = Product f by A6;
hence  a in support b by A1, A2, A4, A7, Th6; ::_thesis: verum
end;
end;
end;

theorem Th7: :: INT_7:7
for p, q being bag of SetPrimes st support p c= support q & p | (support p) = q | (support p) holds
Product p divides Product q
proof
let p, q be bag of SetPrimes ; ::_thesis: ( support p c= support q & p | (support p) = q | (support p) implies Product p divides Product q )
assume that
A1: support p c= support q and
A2: p | (support p) = q | (support p) ; ::_thesis: Product p divides Product q
consider r being bag of SetPrimes  such that
 support r = (support q) \ (support p) and
A3: support p misses support r and
 r | (support r) = q | (support r) and
A4: p + r = q by A1, A2, Lm2;
 (Product p) * (Product r) = Product q by A3, A4, NAT_3:19;
hence  Product p divides Product q by INT_1:def_3; ::_thesis: verum
end;

theorem :: INT_7:8
for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like holds
( x divides Product p iff x in support p ) by Lm4, Lm7;

theorem Th9: :: INT_7:9
for n, m, k being non empty Nat st k = n lcm m holds
support (ppf k) = (support (ppf n)) \/ (support (ppf m))
proof
let n, m, k be non empty Nat; ::_thesis: ( k = n lcm m implies support (ppf k) = (support (ppf n)) \/ (support (ppf m)) )
assume A1: k = n lcm m ; ::_thesis: support (ppf k) = (support (ppf n)) \/ (support (ppf m))
A2: support (ppf n) = support (pfexp n) by NAT_3:def_9;
A3: (support (pfexp n)) \/ (support (pfexp m)) c= support (max ((pfexp n),(pfexp m)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (support (pfexp n)) \/ (support (pfexp m)) or x in support (max ((pfexp n),(pfexp m))) )
assume A4: x in (support (pfexp n)) \/ (support (pfexp m)) ; ::_thesis: x in support (max ((pfexp n),(pfexp m)))
percases ( x in support (pfexp n) or x in support (pfexp m) ) by A4, XBOOLE_0:def_3;
supposeA5: x in support (pfexp n) ; ::_thesis: x in support (max ((pfexp n),(pfexp m)))
A6: (pfexp n) . x <= (max ((pfexp n),(pfexp m))) . x
proof
percases ( (pfexp n) . x <= (pfexp m) . x or (pfexp n) . x > (pfexp m) . x ) ;
suppose (pfexp n) . x <= (pfexp m) . x ; ::_thesis: (pfexp n) . x <= (max ((pfexp n),(pfexp m))) . x
hence  (pfexp n) . x <= (max ((pfexp n),(pfexp m))) . x by NAT_3:def_4; ::_thesis: verum
end;
suppose (pfexp n) . x > (pfexp m) . x ; ::_thesis: (pfexp n) . x <= (max ((pfexp n),(pfexp m))) . x
hence  (pfexp n) . x <= (max ((pfexp n),(pfexp m))) . x by NAT_3:def_4; ::_thesis: verum
end;
end;
end;
 (pfexp n) . x <> 0 by A5, PRE_POLY:def_7;
then  0 < (pfexp n) . x ;
hence  x in support (max ((pfexp n),(pfexp m))) by A6, PRE_POLY:def_7; ::_thesis: verum
end;
supposeA7: x in support (pfexp m) ; ::_thesis: x in support (max ((pfexp n),(pfexp m)))
A8: (pfexp m) . x <= (max ((pfexp n),(pfexp m))) . x
proof
percases ( (pfexp n) . x <= (pfexp m) . x or (pfexp n) . x > (pfexp m) . x ) ;
suppose (pfexp n) . x <= (pfexp m) . x ; ::_thesis: (pfexp m) . x <= (max ((pfexp n),(pfexp m))) . x
hence  (pfexp m) . x <= (max ((pfexp n),(pfexp m))) . x by NAT_3:def_4; ::_thesis: verum
end;
suppose (pfexp n) . x > (pfexp m) . x ; ::_thesis: (pfexp m) . x <= (max ((pfexp n),(pfexp m))) . x
hence  (pfexp m) . x <= (max ((pfexp n),(pfexp m))) . x by NAT_3:def_4; ::_thesis: verum
end;
end;
end;
 (pfexp m) . x <> 0 by A7, PRE_POLY:def_7;
then  0 < (pfexp m) . x ;
hence  x in support (max ((pfexp n),(pfexp m))) by A8, PRE_POLY:def_7; ::_thesis: verum
end;
end;
end;
A9: support (ppf m) = support (pfexp m) by NAT_3:def_9;
A10: support (ppf k) = support (pfexp k) by NAT_3:def_9
.= support (max ((pfexp n),(pfexp m))) by A1, NAT_3:54 ;
then  support (ppf k) c= (support (ppf n)) \/ (support (ppf m)) by A2, A9, NAT_3:18;
hence  support (ppf k) = (support (ppf n)) \/ (support (ppf m)) by A10, A2, A9, A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th10: :: INT_7:10
for X being set
for b1, b2 being bag of X holds support (min (b1,b2)) = (support b1) /\ (support b2)
proof
let X be set ; ::_thesis: for b1, b2 being bag of X holds support (min (b1,b2)) = (support b1) /\ (support b2)
let b1, b2 be bag of X; ::_thesis: support (min (b1,b2)) = (support b1) /\ (support b2)
set f = min (b1,b2);
A1: for x being set st x in support (min (b1,b2)) holds
( x in support b1 & x in support b2 )
proof
let x be set ; ::_thesis: ( x in support (min (b1,b2)) implies ( x in support b1 & x in support b2 ) )
assume A2: x in support (min (b1,b2)) ; ::_thesis: ( x in support b1 & x in support b2 )
assume A3: ( not x in support b1 or not x in support b2 ) ; ::_thesis: contradiction
now__::_thesis:_(_(_b1_._x_<=_b2_._x_&_contradiction_)_or_(_b2_._x_<_b1_._x_&_contradiction_)_)
percases ( b1 . x <= b2 . x or b2 . x < b1 . x ) ;
caseA4: b1 . x <= b2 . x ; ::_thesis: contradiction
A5: not x in support b1
proof
assume A6: x in support b1 ; ::_thesis: contradiction
then A7: b1 . x <> 0 by PRE_POLY:def_7;
 b2 . x = 0 by A3, A6, PRE_POLY:def_7;
hence  contradiction by A4, A7; ::_thesis: verum
end;
(min (b1,b2)) . x = b1 . x by A4, NAT_3:def_3
.= 0 by A5, PRE_POLY:def_7 ;
hence  contradiction by A2, PRE_POLY:def_7; ::_thesis: verum
end;
caseA8: b2 . x < b1 . x ; ::_thesis: contradiction
then (min (b1,b2)) . x = b2 . x by NAT_3:def_3
.= 0 by A3, A8, PRE_POLY:def_7 ;
hence  contradiction by A2, PRE_POLY:def_7; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
 for x being set st x in support b1 & x in support b2 holds
x in support (min (b1,b2))
proof
let x be set ; ::_thesis: ( x in support b1 & x in support b2 implies x in support (min (b1,b2)) )
assume that
A9: x in support b1 and
A10: x in support b2 ; ::_thesis: x in support (min (b1,b2))
A11: b2 . x <> 0 by A10, PRE_POLY:def_7;
A12: ( (min (b1,b2)) . x = b1 . x or (min (b1,b2)) . x = b2 . x ) by NAT_3:def_3;
 b1 . x <> 0 by A9, PRE_POLY:def_7;
hence  x in support (min (b1,b2)) by A11, A12, PRE_POLY:def_7; ::_thesis: verum
end;
hence  support (min (b1,b2)) = (support b1) /\ (support b2) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: INT_7:11
for n, m, k being non empty Nat st k = n gcd m holds
support (ppf k) = (support (ppf n)) /\ (support (ppf m))
proof
let n, m, k be non empty Nat; ::_thesis: ( k = n gcd m implies support (ppf k) = (support (ppf n)) /\ (support (ppf m)) )
assume A1: k = n gcd m ; ::_thesis: support (ppf k) = (support (ppf n)) /\ (support (ppf m))
A2: support (ppf n) = support (pfexp n) by NAT_3:def_9;
A3: support (ppf m) = support (pfexp m) by NAT_3:def_9;
support (ppf k) = support (pfexp k) by NAT_3:def_9
.= support (min ((pfexp n),(pfexp m))) by A1, NAT_3:53 ;
hence  support (ppf k) = (support (ppf n)) /\ (support (ppf m)) by A2, A3, Th10; ::_thesis: verum
end;

theorem Th12: :: INT_7:12
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & support p misses support q holds
Product p, Product q are_relative_prime
proof
let p, q be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like & q is prime-factorization-like & support p misses support q implies Product p, Product q are_relative_prime )
assume that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: support p misses support q ; ::_thesis: Product p, Product q are_relative_prime
assume  not Product p, Product q are_relative_prime ; ::_thesis: contradiction
then consider x being prime Nat such that
A4: x divides Product p and
A5: x divides Product q by PYTHTRIP:def_2;
A6: x in support q by A2, A5, Lm7;
 x in support p by A1, A4, Lm7;
hence  contradiction by A3, A6, XBOOLE_0:3; ::_thesis: verum
end;

Lm8:  for q being Prime
for g being Element of NAT st g <> 0 holds
ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
proof
let q be Prime; ::_thesis: for g being Element of NAT st g <> 0 holds
ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
let g be Element of NAT ; ::_thesis: ( g <> 0 implies ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g ) )
set p = (SetPrimes --> 0) +* (q,g);
reconsider p = (SetPrimes --> 0) +* (q,g) as ManySortedSet of SetPrimes ;
 dom (SetPrimes --> 0) = SetPrimes by FUNCOP_1:13;
then  q in dom (SetPrimes --> 0) by NEWTON:def_6;
then A1: p . q = g by FUNCT_7:31;
A2: for x being set st not x in {q} holds
p . x = 0
proof
let x be set ; ::_thesis: ( not x in {q} implies p . x = 0 )
assume  not x in {q} ; ::_thesis: p . x = 0
then  x <> q by TARSKI:def_1;
hence  p . x = 0 by Lm1; ::_thesis: verum
end;
now__::_thesis:_for_z_being_set_st_z_in_support_p_&_not_z_in_{q}_holds_
z_in_{q}
let z be set ; ::_thesis: ( z in support p & not z in {q} implies z in {q} )
assume A3: z in support p ; ::_thesis: ( not z in {q} implies z in {q} )
 z in dom p
proof
assume  not z in dom p ; ::_thesis: contradiction
then  p . z = {} by FUNCT_1:def_2;
hence  contradiction by A3, PRE_POLY:def_7; ::_thesis: verum
end;
then reconsider y = z as Element of SetPrimes ;
assume  not z in {q} ; ::_thesis: z in {q}
 p . y <> 0 by A3, PRE_POLY:def_7;
hence  z in {q} by A2; ::_thesis: verum
end;
then  for z being set st z in support p holds
z in {q} ;
then A4: support p c= {q} by TARSKI:def_3;
assume A5: g <> 0 ; ::_thesis: ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
now__::_thesis:_for_z_being_set_st_z_in_{q}_holds_
z_in_support_p
let z be set ; ::_thesis: ( z in {q} implies z in support p )
assume  z in {q} ; ::_thesis: z in support p
then A6: z = q by TARSKI:def_1;
thus  z in support p by A5, A1, A6, PRE_POLY:def_7; ::_thesis: verum
end;
then A7: {q} c= support p by TARSKI:def_3;
then A8: support p = {q} by A4, XBOOLE_0:def_10;
reconsider p = p as bag of SetPrimes by A4, PRE_POLY:def_8;
A9: q in support p by A8, TARSKI:def_1;
A10: q in dom p
proof
assume  not q in dom p ; ::_thesis: contradiction
then  p . q = {} by FUNCT_1:def_2;
hence  contradiction by A9, PRE_POLY:def_7; ::_thesis: verum
end;
take  p ; ::_thesis: ( p = (SetPrimes --> 0) +* (q,g) & support p = {q} & Product p = g )
consider f being FinSequence of COMPLEX  such that
A11: Product p = Product f and
A12: f = p * (canFS (support p)) by NAT_3:def_5;
 f = p * <*q*> by A8, A12, UPROOTS:4;
then  f = <*(p . q)*> by A10, FINSEQ_2:34;
hence  ( p = (SetPrimes --> 0) +* (q,g) & support p = {q} & Product p = g ) by A1, A4, A7, A11, RVSUM_1:95, XBOOLE_0:def_10; ::_thesis: verum
end;

Lm9:  for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like & x in support p & p . x = x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x )
proof
let p be bag of SetPrimes ; ::_thesis: for x being Prime st p is prime-factorization-like & x in support p & p . x = x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x )
let x be Prime; ::_thesis: ( p is prime-factorization-like & x in support p & p . x = x implies ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x ) )
assume that
A1: p is prime-factorization-like and
A2: x in support p and
A3: p . x = x ; ::_thesis: ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x )
consider nx being Nat such that
A4: 0 < nx and
A5: p . x = x |^ nx by A1, A2, Def1;
consider mx being Nat such that
A6: nx = mx + 1 by A4, NAT_1:6;
A7: mx = 0
proof
assume  mx <> 0 ; ::_thesis: contradiction
then A8: 0 + 1 < mx + 1 by XREAL_1:8;
 1 < x by INT_2:def_4;
then  x to_power 1 < x to_power nx by A6, A8, POWER:39;
then  x |^ 1 < x to_power nx by POWER:41;
then  x |^ 1 < x |^ nx by POWER:41;
hence  contradiction by A3, A5, NEWTON:5; ::_thesis: verum
end;
 {x} c= support p by A2, ZFMISC_1:31;
then consider q, r being bag of SetPrimes  such that
A9: support q = (support p) \ {x} and
A10: support r = {x} and
A11: support q misses support r and
A12: q | (support q) = p | (support q) and
A13: r | (support r) = p | (support r) and
A14: q + r = p by Lm3;
A15: r = (SetPrimes --> 0) +* (x,(r . x)) by A10, Th1;
now__::_thesis:_for_z_being_Prime_st_z_in_support_q_holds_
ex_n_being_Nat_st_
(_0_<_n_&_q_._z_=_z_|^_n_)
let z be Prime; ::_thesis: ( z in support q implies ex n being Nat st
( 0 < n & q . z = z |^ n ) )
assume A16: z in support q ; ::_thesis: ex n being Nat st
( 0 < n & q . z = z |^ n )
 support q c= support p by A9, XBOOLE_1:36;
then consider n being Nat such that
A17: 0 < n and
A18: p . z = z |^ n by A1, A16, Def1;
take n = n; ::_thesis: ( 0 < n & q . z = z |^ n )
q . z = (q | (support q)) . z by A16, FUNCT_1:49
.= p . z by A12, A16, FUNCT_1:49 ;
hence  ( 0 < n & q . z = z |^ n ) by A17, A18; ::_thesis: verum
end;
then A19: q is prime-factorization-like by Def1;
A20: x in support r by A10, TARSKI:def_1;
then r . x = (r | (support r)) . x by FUNCT_1:49
.= p . x by A13, A20, FUNCT_1:49
.= x by A5, A6, A7, NEWTON:5 ;
then A21: ex rr1 being bag of SetPrimes st
( rr1 = r & support rr1 = {x} & Product rr1 = x ) by A15, Lm8;
 (Product q) * (Product r) = Product p by A11, A14, NAT_3:19;
hence  ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x ) by A9, A12, A19, A21; ::_thesis: verum
end;

Lm10:  for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like & x in support p & p . x <> x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
proof
let p be bag of SetPrimes ; ::_thesis: for x being Prime st p is prime-factorization-like & x in support p & p . x <> x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
let x be Prime; ::_thesis: ( p is prime-factorization-like & x in support p & p . x <> x implies ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x ) )
assume that
A1: p is prime-factorization-like and
A2: x in support p and
A3: p . x <> x ; ::_thesis: ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
consider nx being Nat such that
A4: 0 < nx and
A5: p . x = x |^ nx by A1, A2, Def1;
consider mx being Nat such that
A6: nx = mx + 1 by A4, NAT_1:6;
A7: mx <> 0 by A3, A5, A6, NEWTON:5;
A8: dom (SetPrimes --> 0) = SetPrimes by FUNCOP_1:13;
then A9: x in dom (SetPrimes --> 0) by NEWTON:def_6;
set r10 = (SetPrimes --> 0) +* (x,x);
 x is Element of NAT by ORDINAL1:def_12;
then A10: ex r1 being bag of SetPrimes st
( r1 = (SetPrimes --> 0) +* (x,x) & support r1 = {x} & Product r1 = x ) by Lm8;
A11: {x} c= support p by A2, ZFMISC_1:31;
then consider q, r being bag of SetPrimes  such that
A12: support q = (support p) \ {x} and
A13: support r = {x} and
A14: support q misses support r and
A15: q | (support q) = p | (support q) and
A16: r | (support r) = p | (support r) and
A17: q + r = p by Lm3;
A18: x in support r by A13, TARSKI:def_1;
then A19: r . x = (r | (support r)) . x by FUNCT_1:49
.= p . x by A16, A18, FUNCT_1:49 ;
then A20: (r . x) / x = ((x |^ mx) * x) / x by A5, A6, NEWTON:6
.= x |^ mx by XCMPLX_1:89 ;
then reconsider rxx = (r . x) / x as Element of NAT by ORDINAL1:def_12;
set r20 = (SetPrimes --> 0) +* (x,rxx);
 rxx <> 0
proof
assume A21: rxx = 0 ; ::_thesis: contradiction
r . x = rxx * x by XCMPLX_1:87
.= 0 by A21 ;
hence  contradiction by A5, A19; ::_thesis: verum
end;
then consider r2 being bag of SetPrimes  such that
A22: r2 = (SetPrimes --> 0) +* (x,rxx) and
A23: support r2 = {x} and
A24: Product r2 = rxx by Lm8;
set p1 = q + r2;
A25: r = (SetPrimes --> 0) +* (x,(r . x)) by A13, Th1;
A26: now__::_thesis:_for_z_being_set_st_z_in_(support_(q_+_r2))_\_{x}_holds_
(q_+_r2)_._z_=_p_._z
let z be set ; ::_thesis: ( z in (support (q + r2)) \ {x} implies (q + r2) . z = p . z )
A27: (q + r2) . z = (q . z) + (r2 . z) by PRE_POLY:def_5;
assume A28: z in (support (q + r2)) \ {x} ; ::_thesis: (q + r2) . z = p . z
then  not z in {x} by XBOOLE_0:def_5;
then A29: r2 . z = 0 by A23, PRE_POLY:def_7;
 z in support (q + r2) by A28, XBOOLE_0:def_5;
then  z in (support q) \/ (support r2) by PRE_POLY:38;
then A30: ( z in support q or z in support r2 ) by XBOOLE_0:def_3;
then q . z = (q | (support q)) . z by A23, A28, FUNCT_1:49, XBOOLE_0:def_5
.= p . z by A15, A23, A28, A30, FUNCT_1:49, XBOOLE_0:def_5 ;
hence  (q + r2) . z = p . z by A27, A29; ::_thesis: verum
end;
dom (q + r2) = SetPrimes by PARTFUN1:def_2
.= dom p by PARTFUN1:def_2 ;
then A31: (q + r2) | ((support (q + r2)) \ {x}) = p | ((support (q + r2)) \ {x}) by A26, FUNCT_1:96;
A32: (support q) /\ (support r) = {} by A14, XBOOLE_0:def_7;
now__::_thesis:_for_z_being_Prime_st_z_in_support_(q_+_r2)_holds_
ex_n_being_Nat_st_
(_0_<_n_&_(q_+_r2)_._z_=_z_|^_n_)
let z be Prime; ::_thesis: ( z in support (q + r2) implies ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 ) )
A33: (q + r2) . z = (q . z) + (r2 . z) by PRE_POLY:def_5;
assume  z in support (q + r2) ; ::_thesis: ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 )
then A34: z in (support q) \/ (support r2) by PRE_POLY:38;
percases ( z in support q or z in support r2 ) by A34, XBOOLE_0:def_3;
supposeA35: z in support q ; ::_thesis: ex n being Nat st
( 0 < b2 & (q + r2) . n = n |^ b2 )
then  not z in {x} by A12, XBOOLE_0:def_5;
then A36: r2 . z = 0 by A23, PRE_POLY:def_7;
A37: support q c= support p by A12, XBOOLE_1:36;
q . z = (q | (support q)) . z by A35, FUNCT_1:49
.= p . z by A15, A35, FUNCT_1:49 ;
hence  ex n being Nat st
( 0 < n & (q + r2) . z = z |^ n ) by A1, A33, A35, A37, A36, Def1; ::_thesis: verum
end;
supposeA38: z in support r2 ; ::_thesis: ex mx being Nat st
( 0 < b2 & (q + r2) . mx = mx |^ b2 )
take mx = mx; ::_thesis: ( 0 < mx & (q + r2) . z = z |^ mx )
thus  0 < mx by A7; ::_thesis: (q + r2) . z = z |^ mx
A39: z = x by A23, A38, TARSKI:def_1;
A40: not z in support q by A13, A32, A23, A38, XBOOLE_0:def_4;
(q + r2) . z = (q . z) + (r2 . z) by PRE_POLY:def_5
.= 0 + (r2 . z) by A40, PRE_POLY:def_7
.= z |^ mx by A20, A22, A8, A38, A39, FUNCT_7:31 ;
hence  (q + r2) . z = z |^ mx ; ::_thesis: verum
end;
end;
end;
then A41: q + r2 is prime-factorization-like by Def1;
 x in {x} by TARSKI:def_1;
then A42: not x in support q by A12, XBOOLE_0:def_5;
(q + r2) . x = (q . x) + (r2 . x) by PRE_POLY:def_5
.= 0 + (r2 . x) by A42, PRE_POLY:def_7
.= rxx by A22, A9, FUNCT_7:31 ;
then A43: p . x = ((q + r2) . x) * x by A19, XCMPLX_1:87;
 r . x = rxx * x by XCMPLX_1:87;
then  ex rr1 being bag of SetPrimes st
( rr1 = r & support rr1 = {x} & Product rr1 = rxx * x ) by A5, A19, A25, Lm8;
then A44: Product p = (Product q) * ((Product r2) * x) by A14, A17, A24, NAT_3:19
.= ((Product q) * (Product r2)) * x
.= (Product (q + r2)) * x by A13, A14, A23, NAT_3:19 ;
support (q + r2) = ((support p) \ {x}) \/ {x} by A12, A23, PRE_POLY:38
.= (support p) \/ {x} by XBOOLE_1:39
.= support p by A11, XBOOLE_1:12 ;
hence  ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x ) by A10, A43, A44, A41, A31; ::_thesis: verum
end;

theorem Th13: :: INT_7:13
for p being bag of SetPrimes st p is prime-factorization-like holds
Product p <> 0
proof
let p be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like implies Product p <> 0 )
assume A1: p is prime-factorization-like ; ::_thesis: Product p <> 0
A2: rng (canFS (support p)) = support p by FUNCT_2:def_3;
consider f being FinSequence of COMPLEX  such that
A3: Product p = Product f and
A4: f = p * (canFS (support p)) by NAT_3:def_5;
reconsider f = f as complex-yielding FinSequence ;
assume  Product p = 0 ; ::_thesis: contradiction
then consider k being Nat such that
A5: k in dom f and
A6: f . k = 0 by A3, RVSUM_1:103;
 k in dom (canFS (support p)) by A4, A5, FUNCT_1:11;
then A7: (canFS (support p)) . k in support p by A2, FUNCT_1:3;
then reconsider q = (canFS (support p)) . k as Prime by NEWTON:def_6;
 ex n being Nat st
( 0 < n & p . q = q |^ n ) by A1, A7, Def1;
hence  contradiction by A4, A5, A6, FUNCT_1:12; ::_thesis: verum
end;

theorem Th14: :: INT_7:14
for p being bag of SetPrimes st p is prime-factorization-like holds
( Product p = 1 iff support p = {} )
proof
let p be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like implies ( Product p = 1 iff support p = {} ) )
assume A1: p is prime-factorization-like ; ::_thesis: ( Product p = 1 iff support p = {} )
A2: now__::_thesis:_(_Product_p_=_1_implies_support_p_=_{}_)
assume A3: Product p = 1 ; ::_thesis: support p = {}
thus  support p = {} ::_thesis: verum
proof
assume  support p <> {} ; ::_thesis: contradiction
then consider q being set  such that
A4: q in support p by XBOOLE_0:def_1;
 q in SetPrimes by A4;
then reconsider q = q as Element of NAT ;
reconsider q = q as Prime by A4, NEWTON:def_6;
 q = 1 by A1, A3, A4, Lm4, WSIERP_1:15;
hence  contradiction by INT_2:def_4; ::_thesis: verum
end;
end;
now__::_thesis:_(_support_p_=_{}_implies_Product_p_=_1_)
consider f being FinSequence of COMPLEX  such that
A5: Product p = Product f and
A6: f = p * (canFS (support p)) by NAT_3:def_5;
assume  support p = {} ; ::_thesis: Product p = 1
hence  Product p = 1 by A5, A6, RVSUM_1:94; ::_thesis: verum
end;
hence  ( Product p = 1 iff support p = {} ) by A2; ::_thesis: verum
end;

Lm11:  for n being Element of NAT
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds
p = q
proof
defpred S1[ Element of NAT ] means  for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ $1 & Product p = Product q holds
p = q;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_p,_q_being_bag_of_SetPrimes_st_p_is_prime-factorization-like_&_q_is_prime-factorization-like_&_Product_p_<=_2_|^_(k_+_1)_&_Product_p_=_Product_q_holds_
p_=_q
let p, q be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ (k + 1) & Product p = Product q implies p = q )
assume that
A3: p is prime-factorization-like and
A4: q is prime-factorization-like and
A5: Product p <= 2 |^ (k + 1) and
A6: Product p = Product q ; ::_thesis: p = q
now__::_thesis:_p_=_q
percases ( support p = {} or support p <> {} ) ;
supposeA7: support p = {} ; ::_thesis: p = q
then  Product p = 1 by A3, Th14;
then  support q = {} by A4, A6, Th14;
hence  p = q by A7, Th4; ::_thesis: verum
end;
suppose support p <> {} ; ::_thesis: p = q
then consider x being set  such that
A8: x in support p by XBOOLE_0:def_1;
reconsider x = x as Prime by A8, NEWTON:def_6;
A9: x divides Product p by A3, A8, Lm4;
then A10: x in support q by A4, A6, Lm7;
percases ( p . x <> x or p . x = x ) ;
suppose p . x <> x ; ::_thesis: p = q
then consider p1, r1 being bag of SetPrimes  such that
A11: p1 is prime-factorization-like and
 support r1 = {x} and
 Product r1 = x and
A12: support p1 = support p and
A13: p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) and
A14: p . x = (p1 . x) * x and
A15: Product p = (Product p1) * x by A3, A8, Lm10;
percases ( q . x <> x or q . x = x ) ;
supposeA16: q . x <> x ; ::_thesis: p = q
 1 < x by INT_2:def_4;
then  1 + 1 <= x by NAT_1:13;
then A17: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
consider q1, r2 being bag of SetPrimes  such that
A18: q1 is prime-factorization-like and
 support r2 = {x} and
 Product r2 = x and
A19: support q1 = support q and
A20: q1 | ((support q1) \ {x}) = q | ((support q1) \ {x}) and
A21: q . x = (q1 . x) * x and
A22: Product q = (Product q1) * x by A4, A6, A9, A16, Lm7, Lm10;
 ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A15, XREAL_1:72;
then  ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A17, XXREAL_0:2;
then  Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then  Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A23: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:5;
then A24: p1 = q1 by A2, A6, A11, A15, A18, A22, XCMPLX_1:5;
A25: now__::_thesis:_for_z_being_set_st_z_in_support_p_holds_
p_._z_=_q_._z
let z be set ; ::_thesis: ( z in support p implies p . b1 = q . b1 )
assume A26: z in support p ; ::_thesis: p . b1 = q . b1
percases ( not z in {x} or z in {x} ) ;
suppose not z in {x} ; ::_thesis: p . b1 = q . b1
then A27: z in (support p1) \ {x} by A12, A26, XBOOLE_0:def_5;
hence p . z = (p | ((support p1) \ {x})) . z by FUNCT_1:49
.= q . z by A13, A20, A24, A27, FUNCT_1:49 ;
::_thesis: verum
end;
supposeA28: z in {x} ; ::_thesis: p . b1 = q . b1
hence p . z = (p1 . x) * x by A14, TARSKI:def_1
.= (q1 . x) * x by A2, A6, A11, A15, A18, A22, A23, XCMPLX_1:5
.= q . z by A21, A28, TARSKI:def_1 ;
::_thesis: verum
end;
end;
end;
A29: dom p = SetPrimes by PARTFUN1:def_2
.= dom q by PARTFUN1:def_2 ;
 support p = support q by A2, A6, A11, A12, A15, A18, A19, A22, A23, XCMPLX_1:5;
then  p | (support p) = q | (support q) by A29, A25, FUNCT_1:96;
hence  p = q by Th3; ::_thesis: verum
end;
supposeA30: q . x = x ; ::_thesis: p = q
 1 < x by INT_2:def_4;
then  1 + 1 <= x by NAT_1:13;
then A31: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
 ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A15, XREAL_1:72;
then  ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A31, XXREAL_0:2;
then  Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then  Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A32: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:5;
 ex q1, r2 being bag of SetPrimes st
( q1 is prime-factorization-like & support r2 = {x} & Product r2 = x & support q1 = (support q) \ {x} & q1 | (support q1) = q | (support q1) & Product q = (Product q1) * x ) by A4, A6, A9, A30, Lm7, Lm9;
then  support p = (support q) \ {x} by A2, A6, A11, A12, A15, A32, XCMPLX_1:5;
then  not x in {x} by A8, XBOOLE_0:def_5;
hence  p = q by TARSKI:def_1; ::_thesis: verum
end;
end;
end;
supposeA33: p . x = x ; ::_thesis: p = q
then consider p1, r1 being bag of SetPrimes  such that
A34: p1 is prime-factorization-like and
 support r1 = {x} and
 Product r1 = x and
A35: support p1 = (support p) \ {x} and
A36: p1 | (support p1) = p | (support p1) and
A37: Product p = (Product p1) * x by A3, A8, Lm9;
percases ( q . x <> x or q . x = x ) ;
supposeA38: q . x <> x ; ::_thesis: p = q
 1 < x by INT_2:def_4;
then  1 + 1 <= x by NAT_1:13;
then A39: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
 ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A37, XREAL_1:72;
then  ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A39, XXREAL_0:2;
then  Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then  Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A40: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:5;
 ex q1, r2 being bag of SetPrimes st
( q1 is prime-factorization-like & support r2 = {x} & Product r2 = x & support q1 = support q & q1 | ((support q1) \ {x}) = q | ((support q1) \ {x}) & q . x = (q1 . x) * x & Product q = (Product q1) * x ) by A4, A6, A9, A38, Lm7, Lm10;
then  (support p) \ {x} = support q by A2, A6, A34, A35, A37, A40, XCMPLX_1:5;
then  not x in {x} by A10, XBOOLE_0:def_5;
hence  p = q by TARSKI:def_1; ::_thesis: verum
end;
supposeA41: q . x = x ; ::_thesis: p = q
 1 < x by INT_2:def_4;
then  1 + 1 <= x by NAT_1:13;
then A42: (2 |^ (k + 1)) / x <= (2 |^ (k + 1)) / 2 by XREAL_1:118;
consider q1, r2 being bag of SetPrimes  such that
A43: q1 is prime-factorization-like and
 support r2 = {x} and
 Product r2 = x and
A44: support q1 = (support q) \ {x} and
A45: q1 | (support q1) = q | (support q1) and
A46: Product q = (Product q1) * x by A4, A6, A9, A41, Lm7, Lm9;
 ((Product p1) * x) / x <= (2 |^ (k + 1)) / x by A5, A37, XREAL_1:72;
then  ((Product p1) * x) / x <= (2 |^ (k + 1)) / 2 by A42, XXREAL_0:2;
then  Product p1 <= (2 |^ (k + 1)) / 2 by XCMPLX_1:89;
then  Product p1 <= ((2 |^ k) * (2 |^ 1)) / 2 by NEWTON:8;
then A47: Product p1 <= ((2 |^ k) * 2) / 2 by NEWTON:5;
then  (support p) \ {x} = (support q) \ {x} by A2, A6, A34, A35, A37, A43, A44, A46, XCMPLX_1:5;
then  (support p) \/ {x} = ((support q) \ {x}) \/ {x} by XBOOLE_1:39;
then A48: (support p) \/ {x} = (support q) \/ {x} by XBOOLE_1:39;
A49: p1 = q1 by A2, A6, A34, A37, A43, A46, A47, XCMPLX_1:5;
A50: now__::_thesis:_for_z_being_set_st_z_in_support_p_holds_
p_._z_=_q_._z
let z be set ; ::_thesis: ( z in support p implies p . b1 = q . b1 )
assume A51: z in support p ; ::_thesis: p . b1 = q . b1
percases ( not z in {x} or z in {x} ) ;
suppose not z in {x} ; ::_thesis: p . b1 = q . b1
then A52: z in support p1 by A35, A51, XBOOLE_0:def_5;
hence p . z = (p1 | (support p1)) . z by A36, FUNCT_1:49
.= q . z by A45, A49, A52, FUNCT_1:49 ;
::_thesis: verum
end;
supposeA53: z in {x} ; ::_thesis: p . b1 = q . b1
hence p . z = x by A33, TARSKI:def_1
.= q . z by A41, A53, TARSKI:def_1 ;
::_thesis: verum
end;
end;
end;
A54: {x} c= support q by A10, ZFMISC_1:31;
 {x} c= support p by A8, ZFMISC_1:31;
then A55: support p = (support q) \/ {x} by A48, XBOOLE_1:12;
dom p = SetPrimes by PARTFUN1:def_2
.= dom q by PARTFUN1:def_2 ;
then p | (support p) = q | (support p) by A50, FUNCT_1:96
.= q | (support q) by A54, A55, XBOOLE_1:12 ;
hence  p = q by Th3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
hence  p = q ; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A56: S1[ 0 ]
proof
let p, q be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ 0 & Product p = Product q implies p = q )
assume that
A57: p is prime-factorization-like and
A58: q is prime-factorization-like and
A59: Product p <= 2 |^ 0 and
A60: Product p = Product q ; ::_thesis: p = q
 Product p <> 0 by A57, Th13;
then A61: 0 + 1 <= Product p by NAT_1:13;
 Product p <= 1 by A59, NEWTON:4;
then A62: Product p = 1 by A61, XXREAL_0:1;
then A63: support p = {} by A57, Th14;
 support q = {} by A58, A60, A62, Th14;
hence  p = q by A63, Th4; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A56, A1);
hence  for n being Element of NAT
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds
p = q ; ::_thesis: verum
end;

theorem Th15: :: INT_7:15
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p = Product q holds
p = q
proof
let p, q be bag of SetPrimes ; ::_thesis: ( p is prime-factorization-like & q is prime-factorization-like & Product p = Product q implies p = q )
assume that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: Product p = Product q ; ::_thesis: p = q
reconsider n = Product p as Element of NAT ;
 n <= 2 |^ n by NEWTON:86;
hence  p = q by A1, A2, A3, Lm11; ::_thesis: verum
end;

theorem :: INT_7:16
for p being bag of SetPrimes
for n being non empty Nat st p is prime-factorization-like & n = Product p holds
ppf n = p
proof
let p be bag of SetPrimes ; ::_thesis: for n being non empty Nat st p is prime-factorization-like & n = Product p holds
ppf n = p
let n be non empty Nat; ::_thesis: ( p is prime-factorization-like & n = Product p implies ppf n = p )
assume that
A1: p is prime-factorization-like and
A2: n = Product p ; ::_thesis: ppf n = p
 Product (ppf n) = Product p by A2, NAT_3:61;
hence  ppf n = p by A1, Th15; ::_thesis: verum
end;

theorem Th17: :: INT_7:17
for n, m being Element of NAT st 1 <= n & 1 <= m holds
ex m0, n0 being Element of NAT st
( n lcm m = n0 * m0 & n0 gcd m0 = 1 & n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0 )
proof
let n1, m1 be Element of NAT ; ::_thesis: ( 1 <= n1 & 1 <= m1 implies ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 ) )
assume that
A1: 1 <= n1 and
A2: 1 <= m1 ; ::_thesis: ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 )
reconsider n = n1, m = m1 as non empty Nat by A1, A2;
set nm1 = n1 lcm m1;
reconsider nm = n1 lcm m1 as non empty Nat by A1, A2, INT_2:4;
set N1 =  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ;
set N2 = (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ;
A3:  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  c= support (ppf n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  or x in support (ppf n) )
assume  x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: x in support (ppf n)
then  ex p being Element of NAT st
( x = p & p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) ;
hence  x in support (ppf n) ; ::_thesis: verum
end;
A4: for x being set st x in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  holds
(pfexp nm) . x = (pfexp m) . x
proof
let x be set ; ::_thesis: ( x in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  implies (pfexp nm) . x = (pfexp m) . x )
A5: ( (pfexp n) . x > (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp n) . x ) by NAT_3:def_4;
assume  x in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: (pfexp nm) . x = (pfexp m) . x
then A6: not x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  by XBOOLE_0:def_5;
A7: support (ppf n) = support (pfexp n) by NAT_3:def_9;
A8: not (pfexp n) . x > (pfexp m) . x
proof
assume A9: (pfexp n) . x > (pfexp m) . x ; ::_thesis: contradiction
then A10: (pfexp nm) . x = (pfexp n) . x by A5, NAT_3:54;
A11: x in support (pfexp n) by A9, PRE_POLY:def_7;
then  x in SetPrimes ;
hence  contradiction by A6, A7, A10, A11; ::_thesis: verum
end;
 ( (pfexp n) . x <= (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp m) . x ) by NAT_3:def_4;
hence  (pfexp nm) . x = (pfexp m) . x by A8, NAT_3:54; ::_thesis: verum
end;
A12: Product (ppf m) = m by NAT_3:61;
A13: support (ppf nm) = (support (ppf n)) \/ (support (ppf m)) by Th9;
then A14: support (ppf n) c= support (ppf nm) by XBOOLE_1:7;
then consider ppm, ppn being bag of SetPrimes  such that
A15: support ppm = (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  and
A16: support ppn =  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  and
A17: support ppm misses support ppn and
A18: ppm | (support ppm) = (ppf nm) | (support ppm) and
A19: ppn | (support ppn) = (ppf nm) | (support ppn) and
A20: ppm + ppn = ppf nm by A3, Lm3, XBOOLE_1:1;
reconsider n0 = Product ppn, m0 = Product ppm as Element of NAT ;
A21: Product (ppf n) = n by NAT_3:61;
A22: (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  c= support (ppf m)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  or x in support (ppf m) )
A23: ( (pfexp n) . x <= (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp m) . x ) by NAT_3:def_4;
A24: ( (pfexp n) . x > (pfexp m) . x implies (max ((pfexp n),(pfexp m))) . x = (pfexp n) . x ) by NAT_3:def_4;
assume A25: x in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: x in support (ppf m)
then A26: x in SetPrimes ;
A27: x in support (ppf nm) by A25, XBOOLE_0:def_5;
then  x in support (pfexp nm) by NAT_3:def_9;
then A28: ( (pfexp nm) . x = (pfexp m) . x implies (pfexp m) . x <> 0 ) by PRE_POLY:def_7;
 not x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  by A25, XBOOLE_0:def_5;
then A29: ( not x in support (ppf n) or (pfexp nm) . x <> (pfexp n) . x ) by A26;
 support (ppf m) = support (pfexp m) by NAT_3:def_9;
hence  x in support (ppf m) by A13, A27, A29, A23, A24, A28, NAT_3:54, PRE_POLY:def_7, XBOOLE_0:def_3; ::_thesis: verum
end;
  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  \/ ((support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ) = support (ppf nm) by A14, A3, XBOOLE_1:1, XBOOLE_1:45;
then A30: (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  c= support (ppf nm) by XBOOLE_1:7;
A31: now__::_thesis:_for_x2_being_set_st_x2_in_(support_(ppf_nm))_\__{__p_where_p_is_Element_of_NAT_:_(_p_in_support_(ppf_n)_&_(pfexp_nm)_._p_=_(pfexp_n)_._p_)__}__holds_
(ppf_nm)_._x2_=_(ppf_m)_._x2
let x2 be set ; ::_thesis: ( x2 in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  implies (ppf nm) . x2 = (ppf m) . x2 )
assume A32: x2 in (support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: (ppf nm) . x2 = (ppf m) . x2
then reconsider x = x2 as Prime by NEWTON:def_6;
 x2 in support (ppf m) by A22, A32;
then A33: x2 in support (pfexp m) by NAT_3:def_9;
 x2 in support (ppf nm) by A30, A32;
then  x2 in support (pfexp nm) by NAT_3:def_9;
hence (ppf nm) . x2 = x |^ (x |-count nm) by NAT_3:def_9
.= x |^ ((pfexp nm) . x) by NAT_3:def_8
.= x |^ ((pfexp m) . x) by A4, A32
.= x |^ (x |-count m) by NAT_3:def_8
.= (ppf m) . x2 by A33, NAT_3:def_9 ;
::_thesis: verum
end;
dom (ppf nm) = SetPrimes by PARTFUN1:def_2
.= dom (ppf m) by PARTFUN1:def_2 ;
then  ppm | ((support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ) = (ppf m) | ((support (ppf nm)) \  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ) by A15, A18, A31, FUNCT_1:96;
then A34: m0 divides m by A22, A12, A15, Th7;
A35: n0 * m0 = Product (ppf nm) by A17, A20, NAT_3:19
.= nm by NAT_3:61 ;
then A36: m0 <> 0 ;
now__::_thesis:_for_x_being_Prime_st_x_in_support_ppm_holds_
ex_m_being_Nat_st_
(_0_<_m_&_ppm_._x_=_x_|^_m_)
let x be Prime; ::_thesis: ( x in support ppm implies ex m being Nat st
( 0 < m & ppm . x = x |^ m ) )
assume A37: x in support ppm ; ::_thesis: ex m being Nat st
( 0 < m & ppm . x = x |^ m )
then  x in support (ppf nm) by A15, XBOOLE_0:def_5;
then A38: x in support (pfexp nm) by NAT_3:def_9;
then A39: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def_9;
 (pfexp nm) . x <> 0 by A38, NAT_3:36, NAT_3:38;
then A40: 0 < x |-count nm by NAT_3:def_8;
ppm . x = (ppm | (support ppm)) . x by A37, FUNCT_1:49
.= (ppf nm) . x by A18, A37, FUNCT_1:49 ;
hence  ex m being Nat st
( 0 < m & ppm . x = x |^ m ) by A39, A40; ::_thesis: verum
end;
then A41: ppm is prime-factorization-like by Def1;
A42:  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  c= support (ppf nm) by A14, A3, XBOOLE_1:1;
now__::_thesis:_for_x_being_Prime_st_x_in_support_ppn_holds_
ex_n_being_Nat_st_
(_0_<_n_&_ppn_._x_=_x_|^_n_)
let x be Prime; ::_thesis: ( x in support ppn implies ex n being Nat st
( 0 < n & ppn . x = x |^ n ) )
assume A43: x in support ppn ; ::_thesis: ex n being Nat st
( 0 < n & ppn . x = x |^ n )
then  x in support (ppf nm) by A42, A16;
then A44: x in support (pfexp nm) by NAT_3:def_9;
then A45: (ppf nm) . x = x |^ (x |-count nm) by NAT_3:def_9;
 (pfexp nm) . x <> 0 by A44, NAT_3:36, NAT_3:38;
then A46: 0 < x |-count nm by NAT_3:def_8;
ppn . x = (ppn | (support ppn)) . x by A43, FUNCT_1:49
.= (ppf nm) . x by A19, A43, FUNCT_1:49 ;
hence  ex n being Nat st
( 0 < n & ppn . x = x |^ n ) by A45, A46; ::_thesis: verum
end;
then  ppn is prime-factorization-like by Def1;
then  n0,m0 are_relative_prime by A17, A41, Th12;
then A47: n0 gcd m0 = 1 by INT_2:def_3;
A48: for x being set st x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  holds
(pfexp nm) . x = (pfexp n) . x
proof
let x be set ; ::_thesis: ( x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  implies (pfexp nm) . x = (pfexp n) . x )
assume  x in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: (pfexp nm) . x = (pfexp n) . x
then  ex p being Element of NAT st
( x = p & p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p ) ;
hence  (pfexp nm) . x = (pfexp n) . x ; ::_thesis: verum
end;
A49: now__::_thesis:_for_x1_being_set_st_x1_in__{__p_where_p_is_Element_of_NAT_:_(_p_in_support_(ppf_n)_&_(pfexp_nm)_._p_=_(pfexp_n)_._p_)__}__holds_
(ppf_nm)_._x1_=_(ppf_n)_._x1
let x1 be set ; ::_thesis: ( x1 in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  implies (ppf nm) . x1 = (ppf n) . x1 )
assume A50: x1 in  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  ; ::_thesis: (ppf nm) . x1 = (ppf n) . x1
then A51: x1 in support (ppf nm) by A42;
then reconsider x = x1 as Prime by NEWTON:def_6;
 x1 in support (ppf n) by A3, A50;
then A52: x1 in support (pfexp n) by NAT_3:def_9;
 x1 in support (pfexp nm) by A51, NAT_3:def_9;
hence (ppf nm) . x1 = x |^ (x |-count nm) by NAT_3:def_9
.= x |^ ((pfexp nm) . x) by NAT_3:def_8
.= x |^ ((pfexp n) . x) by A48, A50
.= x |^ (x |-count n) by NAT_3:def_8
.= (ppf n) . x1 by A52, NAT_3:def_9 ;
::_thesis: verum
end;
dom (ppf nm) = SetPrimes by PARTFUN1:def_2
.= dom (ppf n) by PARTFUN1:def_2 ;
then A53: ppn |  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  = (ppf n) |  {  p where p is Element of NAT : ( p in support (ppf n) & (pfexp nm) . p = (pfexp n) . p )  }  by A16, A19, A49, FUNCT_1:96;
 n0 <> 0 by A35;
hence  ex m0, n0 being Element of NAT st
( n1 lcm m1 = n0 * m0 & n0 gcd m0 = 1 & n0 divides n1 & m0 divides m1 & n0 <> 0 & m0 <> 0 ) by A3, A21, A16, A53, A35, A34, A36, A47, Th7; ::_thesis: verum
end;

begin

definition
let n be Nat;
assume A1: 1 < n ;
func Segm0 n ->  non empty finite Subset of NAT equals :Def2: :: INT_7:def 2
(Segm n) \ {0};
correctness
coherence
(Segm n) \ {0} is non empty finite Subset of NAT;
proof
A2: not 1 in {0} by TARSKI:def_1;
 1 in Segm n by A1, NAT_1:44;
hence  (Segm n) \ {0} is non empty finite Subset of NAT by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Segm0 INT_7:def_2_:_
 for n being Nat st 1 < n holds
Segm0 n = (Segm n) \ {0};

theorem Th18: :: INT_7:18
for n being Nat st 1 < n holds
card (Segm0 n) = n - 1
proof
let n be Nat; ::_thesis: ( 1 < n implies card (Segm0 n) = n - 1 )
A1: card (Segm n) = n by CARD_1:def_2;
assume A2: 1 < n ; ::_thesis: card (Segm0 n) = n - 1
then A3: 0 in Segm n by NAT_1:44;
A4: card {0} = 1 by CARD_1:30;
 Segm0 n = (Segm n) \ {0} by A2, Def2;
hence  card (Segm0 n) = n - 1 by A1, A3, A4, EULER_1:4; ::_thesis: verum
end;

definition
let n be Prime;
func multint0 n ->  BinOp of (Segm0 n) equals :: INT_7:def 3
(multint n) || (Segm0 n);
coherence
 (multint n) || (Segm0 n) is BinOp of (Segm0 n)
proof
A1: 1 < n by INT_2:def_4;
then  Segm0 n = (Segm n) \ {0} by Def2;
then reconsider S = Segm0 n as Subset of (Segm n) by XBOOLE_1:36;
 multint n is Presv of Segm n,S
proof
let x be set ; :: according to REALSET1:def_4 ::_thesis: ( not x in [:S,S:] or (multint n) . x in S )
A2: 0 in Segm n by NAT_1:44;
assume  x in [:S,S:] ; ::_thesis: (multint n) . x in S
then consider a, b being set  such that
A3: a in Segm0 n and
A4: b in Segm0 n and
A5: x = [a,b] by ZFMISC_1:def_2;
A6: b in (Segm n) \ {0} by A1, A4, Def2;
then reconsider b1 = b as Element of (INT.Ring n) by XBOOLE_0:def_5;
 not b in {0} by A6, XBOOLE_0:def_5;
then  b <> 0 by TARSKI:def_1;
then A7: b <> 0. (INT.Ring n) by A2, FUNCT_7:def_1;
A8: a in (Segm n) \ {0} by A1, A3, Def2;
then reconsider a1 = a as Element of (INT.Ring n) by XBOOLE_0:def_5;
set y = (multint n) . (a,b);
A9: (multint n) . (a,b) = a1 * b1 ;
 not a in {0} by A8, XBOOLE_0:def_5;
then  a <> 0 by TARSKI:def_1;
then  a <> 0. (INT.Ring n) by A2, FUNCT_7:def_1;
then  (multint n) . (a,b) <> In (0,(Segm n)) by A9, A7, VECTSP_1:12;
then  (multint n) . (a,b) <> 0 by A9, FUNCT_7:def_1;
then  not (multint n) . (a,b) in {0} by TARSKI:def_1;
then  (multint n) . (a,b) in (Segm n) \ {0} by A9, XBOOLE_0:def_5;
hence  (multint n) . x in S by A1, A5, Def2; ::_thesis: verum
end;
hence  (multint n) || (Segm0 n) is BinOp of (Segm0 n) by REALSET1:6; ::_thesis: verum
end;
end;

:: deftheorem  defines multint0 INT_7:def_3_:_
 for n being Prime holds multint0 n = (multint n) || (Segm0 n);

Lm12:  for p being Prime
for a, b being Element of multMagma(# (Segm0 p),(multint0 p) #)
for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
proof
let p be Prime; ::_thesis: for a, b being Element of multMagma(# (Segm0 p),(multint0 p) #)
for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
let a, b be Element of multMagma(# (Segm0 p),(multint0 p) #); ::_thesis: for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
let x, y be Element of (INT.Ring p); ::_thesis: ( a = x & y = b implies x * y = a * b )
assume that
A1: a = x and
A2: y = b ; ::_thesis: x * y = a * b
thus a * b = (multint p) . [a,b] by FUNCT_1:49
.= x * y by A1, A2 ; ::_thesis: verum
end;

theorem Th19: :: INT_7:19
for p being Prime holds
( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )
proof
let p be Prime; ::_thesis: ( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like )
set Zp = multMagma(# (Segm0 p),(multint0 p) #);
A1: not 1 in {0} by TARSKI:def_1;
A2: 1 < p by INT_2:def_4;
then  1 in Segm p by NAT_1:44;
then  1 in (Segm p) \ {0} by A1, XBOOLE_0:def_5;
then  1 in Segm0 p by A2, Def2;
then reconsider e = 1. (INT.Ring p) as Element of multMagma(# (Segm0 p),(multint0 p) #) by A2, INT_3:14;
A3: multMagma(# (Segm0 p),(multint0 p) #) is associative
proof
let x, y, z be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
 x in Segm0 p ;
then  x in (Segm p) \ {0} by A2, Def2;
then reconsider x1 = x as Element of (INT.Ring p) by XBOOLE_0:def_5;
 y in Segm0 p ;
then  y in (Segm p) \ {0} by A2, Def2;
then reconsider y1 = y as Element of (INT.Ring p) by XBOOLE_0:def_5;
 z in Segm0 p ;
then  z in (Segm p) \ {0} by A2, Def2;
then reconsider z1 = z as Element of (INT.Ring p) by XBOOLE_0:def_5;
A4: y * z = y1 * z1 by Lm12;
 x * y = x1 * y1 by Lm12;
then (x * y) * z = (x1 * y1) * z1 by Lm12
.= x1 * (y1 * z1) by GROUP_1:def_3
.= x * (y * z) by A4, Lm12 ;
hence  (x * y) * z = x * (y * z) ; ::_thesis: verum
end;
A5: now__::_thesis:_for_h_being_Element_of_multMagma(#_(Segm0_p),(multint0_p)_#)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_&_ex_g_being_Element_of_multMagma(#_(Segm0_p),(multint0_p)_#)_st_
(_h_*_g_=_e_&_g_*_h_=_e_)_)
let h be Element of multMagma(# (Segm0 p),(multint0 p) #); ::_thesis: ( h * e = h & e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )
 h in Segm0 p ;
then A6: h in (Segm p) \ {0} by A2, Def2;
then reconsider hp = h as Element of (INT.Ring p) by XBOOLE_0:def_5;
thus h * e = hp * (1_ (INT.Ring p)) by Lm12
.= h by GROUP_1:def_4 ; ::_thesis: ( e * h = h & ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) )
thus e * h = (1_ (INT.Ring p)) * hp by Lm12
.= h by GROUP_1:def_4 ; ::_thesis: ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e )
 not h in {0} by A6, XBOOLE_0:def_5;
then A7: hp <> 0 by TARSKI:def_1;
 0 in Segm p by NAT_1:44;
then  hp <> 0. (INT.Ring p) by A7, FUNCT_7:def_1;
then consider hpd being Element of (INT.Ring p) such that
A8: hpd * hp = 1. (INT.Ring p) by VECTSP_1:def_9;
 hpd <> 0. (INT.Ring p) by A8, VECTSP_1:6;
then  hpd <> 0 by FUNCT_7:def_1;
then  not hpd in {0} by TARSKI:def_1;
then  hpd in (Segm p) \ {0} by XBOOLE_0:def_5;
then reconsider g = hpd as Element of multMagma(# (Segm0 p),(multint0 p) #) by A2, Def2;
A9: g * h = e by A8, Lm12;
 h * g = e by A8, Lm12;
hence  ex g being Element of multMagma(# (Segm0 p),(multint0 p) #) st
( h * g = e & g * h = e ) by A9; ::_thesis: verum
end;
 multMagma(# (Segm0 p),(multint0 p) #) is commutative
proof
let x, y be Element of multMagma(# (Segm0 p),(multint0 p) #); :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
 x in Segm0 p ;
then  x in (Segm p) \ {0} by A2, Def2;
then reconsider x1 = x as Element of (INT.Ring p) by XBOOLE_0:def_5;
 y in Segm0 p ;
then  y in (Segm p) \ {0} by A2, Def2;
then reconsider y1 = y as Element of (INT.Ring p) by XBOOLE_0:def_5;
x * y = x1 * y1 by Lm12
.= y * x by Lm12 ;
hence  x * y = y * x ; ::_thesis: verum
end;
hence  ( multMagma(# (Segm0 p),(multint0 p) #) is associative & multMagma(# (Segm0 p),(multint0 p) #) is commutative & multMagma(# (Segm0 p),(multint0 p) #) is Group-like ) by A5, A3, GROUP_1:def_2; ::_thesis: verum
end;

definition
let p be Prime;
func Z/Z* p ->  commutative Group equals :: INT_7:def 4
 multMagma(# (Segm0 p),(multint0 p) #);
correctness
coherence
multMagma(# (Segm0 p),(multint0 p) #) is commutative Group;
by Th19;
end;

:: deftheorem  defines Z/Z* INT_7:def_4_:_
 for p being Prime holds Z/Z* p = multMagma(# (Segm0 p),(multint0 p) #);

theorem :: INT_7:20
for p being Prime
for x, y being Element of (Z/Z* p)
for x1, y1 being Element of (INT.Ring p) st x = x1 & y = y1 holds
x * y = x1 * y1 by Lm12;

theorem Th21: :: INT_7:21
for p being Prime holds
( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) )
proof
let p be Prime; ::_thesis: ( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) )
A1: not 1 in {0} by TARSKI:def_1;
A2: 1 < p by INT_2:def_4;
then  1 in Segm p by NAT_1:44;
then  1 in (Segm p) \ {0} by A1, XBOOLE_0:def_5;
then  1 in Segm0 p by A2, Def2;
then reconsider e = 1. (INT.Ring p) as Element of (Z/Z* p) by A2, INT_3:14;
now__::_thesis:_for_h_being_Element_of_(Z/Z*_p)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (Z/Z* p); ::_thesis: ( h * e = h & e * h = h )
 h in Segm0 p ;
then  h in (Segm p) \ {0} by A2, Def2;
then reconsider hp = h as Element of (INT.Ring p) by XBOOLE_0:def_5;
thus h * e = hp * (1_ (INT.Ring p)) by Lm12
.= h by GROUP_1:def_4 ; ::_thesis: e * h = h
thus e * h = (1_ (INT.Ring p)) * hp by Lm12
.= h by GROUP_1:def_4 ; ::_thesis: verum
end;
then  e = 1_ (Z/Z* p) by GROUP_1:def_4;
hence  ( 1_ (Z/Z* p) = 1 & 1_ (Z/Z* p) = 1. (INT.Ring p) ) by A2, INT_3:14; ::_thesis: verum
end;

theorem :: INT_7:22
for p being Prime
for x being Element of (Z/Z* p)
for x1 being Element of (INT.Ring p) st x = x1 holds
x " = x1 "
proof
let p be Prime; ::_thesis: for x being Element of (Z/Z* p)
for x1 being Element of (INT.Ring p) st x = x1 holds
x " = x1 "
let h be Element of (Z/Z* p); ::_thesis: for x1 being Element of (INT.Ring p) st h = x1 holds
h " = x1 "
let hp be Element of (INT.Ring p); ::_thesis: ( h = hp implies h " = hp " )
assume A1: h = hp ; ::_thesis: h " = hp "
A2: 0 in Segm p by NAT_1:44;
set hpd = hp " ;
A3: 1 < p by INT_2:def_4;
 h in Segm0 p ;
then  h in (Segm p) \ {0} by A3, Def2;
then  not h in {0} by XBOOLE_0:def_5;
then  hp <> 0 by A1, TARSKI:def_1;
then A4: hp <> 0. (INT.Ring p) by A2, FUNCT_7:def_1;
then  hp * (hp ") = 1. (INT.Ring p) by VECTSP_1:def_10;
then  hp " <> 0. (INT.Ring p) by VECTSP_1:6;
then  hp " <> 0 by FUNCT_7:def_1;
then  not hp " in {0} by TARSKI:def_1;
then  hp " in (Segm p) \ {0} by XBOOLE_0:def_5;
then reconsider g = hp " as Element of (Z/Z* p) by A3, Def2;
h * g = hp * (hp ") by A1, Lm12
.= 1. (INT.Ring p) by A4, VECTSP_1:def_10
.= 1_ (Z/Z* p) by Th21 ;
hence  h " = hp " by GROUP_1:def_5; ::_thesis: verum
end;

registration
let p be Prime;
cluster Z/Z* p ->  finite commutative ;
coherence
 Z/Z* p is finite ;
end;

theorem :: INT_7:23
for p being Prime holds card (Z/Z* p) = p - 1
proof
let p be Prime; ::_thesis: card (Z/Z* p) = p - 1
 1 < p by INT_2:def_4;
hence  card (Z/Z* p) = p - 1 by Th18; ::_thesis: verum
end;

theorem :: INT_7:24
for G being Group
for a being Element of G
for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
proof
let G be Group; ::_thesis: for a being Element of G
for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
let a be Element of G; ::_thesis: for i being Integer st not a is being_of_order_0 holds
ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
let i be Integer; ::_thesis: ( not a is being_of_order_0 implies ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) )
assume  not a is being_of_order_0 ; ::_thesis: ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i )
then  ord a <> 0 by GROUP_1:def_11;
then A1: abs i <= (abs i) * (ord a) by NAT_1:14, XREAL_1:151;
 0 <= ((abs i) * (ord a)) + i
proof
percases ( i < 0 or 0 <= i ) ;
supposeA2: i < 0 ; ::_thesis: 0 <= ((abs i) * (ord a)) + i
A3: (abs i) + i <= ((abs i) * (ord a)) + i by A1, XREAL_1:6;
 abs i = - i by A2, ABSVALUE:def_1;
hence  0 <= ((abs i) * (ord a)) + i by A3; ::_thesis: verum
end;
suppose 0 <= i ; ::_thesis: 0 <= ((abs i) * (ord a)) + i
hence  0 <= ((abs i) * (ord a)) + i ; ::_thesis: verum
end;
end;
end;
then A4: ((abs i) * (ord a)) + i is Element of NAT by INT_1:3;
a |^ (((abs i) * (ord a)) + i) = (a |^ ((abs i) * (ord a))) * (a |^ i) by GROUP_1:33
.= ((a |^ (ord a)) |^ (abs i)) * (a |^ i) by GROUP_1:35
.= ((1_ G) |^ (abs i)) * (a |^ i) by GROUP_1:41
.= (1_ G) * (a |^ i) by GROUP_1:31
.= a |^ i by GROUP_1:def_4 ;
hence  ex n, k being Element of NAT st
( a |^ i = a |^ n & n = (k * (ord a)) + i ) by A4; ::_thesis: verum
end;

theorem Th25: :: INT_7:25
for G being commutative Group
for a, b being Element of G
for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
proof
let G be commutative Group; ::_thesis: for a, b being Element of G
for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
let a, b be Element of G; ::_thesis: for n, m being Nat st G is finite & ord a = n & ord b = m & n gcd m = 1 holds
ord (a * b) = n * m
let n, m be Nat; ::_thesis: ( G is finite & ord a = n & ord b = m & n gcd m = 1 implies ord (a * b) = n * m )
assume that
A1: G is finite and
A2: ord a = n and
A3: ord b = m and
A4: n gcd m = 1 ; ::_thesis: ord (a * b) = n * m
 not b is being_of_order_0 by A1, GR_CY_1:6;
then A5: m <> 0 by A3, GROUP_1:def_11;
A6: not a * b is being_of_order_0 by A1, GR_CY_1:6;
A7: (a * b) |^ (n * m) = (a |^ (n * m)) * (b |^ (n * m)) by GROUP_1:48
.= ((a |^ n) |^ m) * (b |^ (n * m)) by GROUP_1:35
.= ((a |^ n) |^ m) * ((b |^ m) |^ n) by GROUP_1:35
.= ((1_ G) |^ m) * ((b |^ m) |^ n) by A2, GROUP_1:41
.= ((1_ G) |^ m) * ((1_ G) |^ n) by A3, GROUP_1:41
.= (1_ G) * ((1_ G) |^ n) by GROUP_1:31
.= (1_ G) * (1_ G) by GROUP_1:31
.= 1_ G by GROUP_1:def_4 ;
A8: m * n is Element of NAT by ORDINAL1:def_12;
reconsider n1 = n, m1 = m as Integer ;
A9: n1,m1 are_relative_prime by A4, INT_2:def_3;
 not a is being_of_order_0 by A1, GR_CY_1:6;
then A10: n <> 0 by A2, GROUP_1:def_11;
A11: now__::_thesis:_for_k_being_Nat_st_(a_*_b)_|^_k_=_1__G_&_k_<>_0_holds_
m_*_n_<=_k
let k be Nat; ::_thesis: ( (a * b) |^ k = 1_ G & k <> 0 implies m * n <= k )
assume that
A12: (a * b) |^ k = 1_ G and
A13: k <> 0 ; ::_thesis: m * n <= k
reconsider k1 = k as Integer ;
1_ G = (1_ G) |^ n by GROUP_1:31
.= (a * b) |^ (k * n) by A12, GROUP_1:35
.= (a |^ (k * n)) * (b |^ (k * n)) by GROUP_1:48
.= ((a |^ n) |^ k) * (b |^ (k * n)) by GROUP_1:35
.= ((1_ G) |^ k) * (b |^ (k * n)) by A2, GROUP_1:41
.= (1_ G) * (b |^ (k * n)) by GROUP_1:31
.= b |^ (k * n) by GROUP_1:def_4 ;
then  m1 divides k1 by A3, A9, GROUP_1:44, INT_2:25;
then consider i being Integer such that
A14: k1 = m1 * i by INT_1:def_3;
1_ G = (1_ G) |^ m by GROUP_1:31
.= (a * b) |^ (k * m) by A12, GROUP_1:35
.= (a |^ (k * m)) * (b |^ (k * m)) by GROUP_1:48
.= (a |^ (k * m)) * ((b |^ m) |^ k) by GROUP_1:35
.= (a |^ (k * m)) * ((1_ G) |^ k) by A3, GROUP_1:41
.= (a |^ (k * m)) * (1_ G) by GROUP_1:31
.= a |^ (k * m) by GROUP_1:def_4 ;
then  n1 divides k1 by A2, A9, GROUP_1:44, INT_2:25;
then  n1 divides i by A9, A14, INT_2:25;
then consider j being Integer such that
A15: i = n1 * j by INT_1:def_3;
 k1 = (m1 * n1) * j by A14, A15;
then  k / (m * n) = j by A10, A5, XCMPLX_1:6, XCMPLX_1:89;
then A16: j is Element of NAT by INT_1:3;
 j <> 0 by A13, A14, A15;
then  (m * n) * 1 <= (m * n) * j by A16, NAT_1:14, XREAL_1:64;
hence  m * n <= k by A14, A15; ::_thesis: verum
end;
 n * m <> 0 by A10, A5, XCMPLX_1:6;
hence  ord (a * b) = n * m by A6, A7, A8, A11, GROUP_1:def_11; ::_thesis: verum
end;

Lm13:  for L being Field
for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n )
proof
let L be Field; ::_thesis: for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n )
defpred S1[ Nat] means  for f being non-zero Polynomial of L st deg f = $1 holds
ex m being Element of NAT st
( m = card (Roots f) & m <= $1 );
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
now__::_thesis:_for_f_being_non-zero_Polynomial_of_L_st_deg_f_=_k_+_1_holds_
ex_m_being_Element_of_NAT_st_
(_m_=_card_(Roots_f)_&_m_<=_k_+_1_)
let f be non-zero Polynomial of L; ::_thesis: ( deg f = k + 1 implies ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) )
A3: f <> 0_. L by UPROOTS:def_5;
assume A4: deg f = k + 1 ; ::_thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )
thus  ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) ::_thesis: verum
proof
percases ( Roots f = {} or Roots f <> {} ) ;
suppose Roots f = {} ; ::_thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )
hence  ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) ; ::_thesis: verum
end;
supposeA5: Roots f <> {} ; ::_thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 )
set RF = Roots f;
consider z being set  such that
A6: z in Roots f by A5, XBOOLE_0:def_1;
reconsider z = z as Element of L by A6;
set g = f div (rpoly (1,z));
A7: z is_a_root_of f by A6, POLYNOM5:def_9;
then  rpoly (1,z) divides f by HURWITZ:35;
then  0_. L = f mod (rpoly (1,z)) by HURWITZ:def_7;
then  (f div (rpoly (1,z))) *' (rpoly (1,z)) = (f - ((f div (rpoly (1,z))) *' (rpoly (1,z)))) + ((f div (rpoly (1,z))) *' (rpoly (1,z))) by POLYNOM3:28;
then  (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + ((- ((f div (rpoly (1,z))) *' (rpoly (1,z)))) + ((f div (rpoly (1,z))) *' (rpoly (1,z)))) by POLYNOM3:26;
then  (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + (((f div (rpoly (1,z))) *' (rpoly (1,z))) - ((f div (rpoly (1,z))) *' (rpoly (1,z)))) ;
then  (f div (rpoly (1,z))) *' (rpoly (1,z)) = f + (0_. L) by POLYNOM3:29;
then A8: f = (f div (rpoly (1,z))) *' (rpoly (1,z)) by POLYNOM3:28;
then  f div (rpoly (1,z)) <> 0_. L by A3, POLYNOM3:34;
then reconsider g = f div (rpoly (1,z)) as non-zero Polynomial of L by UPROOTS:def_5;
set RG = Roots g;
deg g = (k + 1) - 1 by A3, A4, A7, HURWITZ:36
.= k ;
then  ex m1 being Element of NAT st
( m1 = card (Roots g) & m1 <= k ) by A2;
then A9: (card (Roots g)) + 1 <= k + 1 by XREAL_1:6;
 Roots f c= (Roots g) \/ {z}
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Roots f or y in (Roots g) \/ {z} )
assume A10: y in Roots f ; ::_thesis: y in (Roots g) \/ {z}
then reconsider y1 = y as Element of L ;
 y1 is_a_root_of f by A10, POLYNOM5:def_9;
then  eval (f,y1) = 0. L by POLYNOM5:def_6;
then  (eval (g,y1)) * (eval ((rpoly (1,z)),y1)) = 0. L by A8, POLYNOM4:24;
then A11: (eval (g,y1)) * (y1 - z) = 0. L by HURWITZ:29;
now__::_thesis:_y_in_(Roots_g)_\/_{z}
percases ( y1 = z or y1 <> z ) ;
suppose y1 = z ; ::_thesis: y in (Roots g) \/ {z}
then  y in {z} by TARSKI:def_1;
hence  y in (Roots g) \/ {z} by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y1 <> z ; ::_thesis: y in (Roots g) \/ {z}
then  y1 - z <> 0. L by RLVECT_1:21;
then  eval (g,y1) = 0. L by A11, VECTSP_1:12;
then  y1 is_a_root_of g by POLYNOM5:def_6;
then  y1 in Roots g by POLYNOM5:def_9;
hence  y in (Roots g) \/ {z} by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  y in (Roots g) \/ {z} ; ::_thesis: verum
end;
then A12: card (Roots f) <= card ((Roots g) \/ {z}) by NAT_1:43;
 card ((Roots g) \/ {z}) <= (card (Roots g)) + (card {z}) by CARD_2:43;
then  card ((Roots g) \/ {z}) <= (card (Roots g)) + 1 by CARD_2:42;
then  card (Roots f) <= (card (Roots g)) + 1 by A12, XXREAL_0:2;
hence  ex m being Element of NAT st
( m = card (Roots f) & m <= k + 1 ) by A9, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A13: S1[ 0 ]
proof
let f be non-zero Polynomial of L; ::_thesis: ( deg f = 0 implies ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) )
assume A14: deg f = 0 ; ::_thesis: ex m being Element of NAT st
( m = card (Roots f) & m <= 0 )
reconsider x = f . 0 as Element of L ;
A15: f <> 0_. L by UPROOTS:def_5;
A16: f . 0 <> 0. L
proof
assume  f . 0 = 0. L ; ::_thesis: contradiction
then  f = <%(0. L)%> by A14, ALGSEQ_1:def_5;
hence  contradiction by A15, POLYNOM5:34; ::_thesis: verum
end;
A17: now__::_thesis:_for_z_being_Element_of_L_holds_eval_(<%x%>,z)_<>_0._L
let z be Element of L; ::_thesis: eval (<%x%>,z) <> 0. L
eval (<%x%>,z) = eval (<%x,(0. L)%>,z) by POLYNOM5:43
.= x by POLYNOM5:45 ;
hence  eval (<%x%>,z) <> 0. L by A16; ::_thesis: verum
end;
A18: f = <%x%> by A14, ALGSEQ_1:def_5;
 Roots f = {}
proof
assume  Roots f <> {} ; ::_thesis: contradiction
then consider z being set  such that
A19: z in Roots f by XBOOLE_0:def_1;
reconsider z = z as Element of L by A19;
 z is_a_root_of f by A19, POLYNOM5:def_9;
then  eval (<%x%>,z) = 0. L by A18, POLYNOM5:def_6;
hence  contradiction by A17; ::_thesis: verum
end;
hence  ex m being Element of NAT st
( m = card (Roots f) & m <= 0 ) ; ::_thesis: verum
end;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A13, A1);
hence  for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n ) ; ::_thesis: verum
end;

theorem Th26: :: INT_7:26
for L being non empty ZeroStr
for p being Polynomial of L st 0 <= deg p holds
p is non-zero
proof
let L be non empty ZeroStr ; ::_thesis: for p being Polynomial of L st 0 <= deg p holds
p is non-zero
let p be Polynomial of L; ::_thesis: ( 0 <= deg p implies p is non-zero )
assume  0 <= deg p ; ::_thesis: p is non-zero
then  deg p <> - 1 ;
then  p <> 0_. L by HURWITZ:20;
hence  p is non-zero by UPROOTS:def_5; ::_thesis: verum
end;

theorem Th27: :: INT_7:27
for L being Field
for f being Polynomial of L st 0 <= deg f holds
( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )
proof
let L be Field; ::_thesis: for f being Polynomial of L st 0 <= deg f holds
( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )
let f be Polynomial of L; ::_thesis: ( 0 <= deg f implies ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) ) )
assume A1: 0 <= deg f ; ::_thesis: ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) )
then reconsider n = deg f as Element of NAT by INT_1:3;
reconsider f = f as non-zero Polynomial of L by A1, Th26;
 ex m being Element of NAT st
( m = card (Roots f) & m <= n ) by Lm13;
hence  ( Roots f is finite set & ex m, n being Element of NAT st
( n = deg f & m = card (Roots f) & m <= n ) ) ; ::_thesis: verum
end;

theorem Th28: :: INT_7:28
for p being Prime
for z being Element of (Z/Z* p)
for y being Element of (INT.Ring p) st z = y holds
for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
proof
let p be Prime; ::_thesis: for z being Element of (Z/Z* p)
for y being Element of (INT.Ring p) st z = y holds
for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
let z be Element of (Z/Z* p); ::_thesis: for y being Element of (INT.Ring p) st z = y holds
for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
let y be Element of (INT.Ring p); ::_thesis: ( z = y implies for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n) )
defpred S1[ Nat] means (power (Z/Z* p)) . (z,$1) = (power (INT.Ring p)) . (y,$1);
assume A1: z = y ; ::_thesis: for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n)
A2: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
(power (Z/Z* p)) . (z,(k + 1)) = ((power (Z/Z* p)) . (z,k)) * z by GROUP_1:def_7
.= ((power (INT.Ring p)) . (y,k)) * y by A1, A3, Lm12
.= (power (INT.Ring p)) . (y,(k + 1)) by GROUP_1:def_7 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(power (Z/Z* p)) . (z,0) = 1_ (Z/Z* p) by GROUP_1:def_7
.= 1_ (INT.Ring p) by Th21
.= (power (INT.Ring p)) . (y,0) by GROUP_1:def_7 ;
then A4: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A4, A2);
hence  for n being Element of NAT holds (power (Z/Z* p)) . (z,n) = (power (INT.Ring p)) . (y,n) ; ::_thesis: verum
end;

Lm14:  for p being Prime
for L being Field
for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) )
proof
let p be Prime; ::_thesis: for L being Field
for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) )
let L be Field; ::_thesis: for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) )
let n be Nat; ::_thesis: ( 0 < n & L = INT.Ring p implies ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) ) )
assume that
A1: 0 < n and
A2: L = INT.Ring p ; ::_thesis: ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) )
set qq = 1_. L;
reconsider n0 = n as Element of NAT by ORDINAL1:def_12;
set f = (<%(0. L),(1. L)%> `^ n0) - (1_. L);
set pp = <%(0. L),(1. L)%> `^ n0;
A3: now__::_thesis:_for_x_being_Element_of_L
for_xz_being_Element_of_(Z/Z*_p)
for_xn_being_Element_of_(INT.Ring_p)_st_x_=_xz_&_xn_=_xz_|^_n_holds_
eval_(((<%(0._L),(1._L)%>_`^_n0)_-_(1_._L)),x)_=_xn_-_(1__(INT.Ring_p))
let x be Element of L; ::_thesis: for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
let xz be Element of (Z/Z* p); ::_thesis: for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
let xn be Element of (INT.Ring p); ::_thesis: ( x = xz & xn = xz |^ n implies eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p)) )
assume that
A4: x = xz and
A5: xn = xz |^ n ; ::_thesis: eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = xn - (1_ (INT.Ring p))
A6: xn = xz |^ n0 by A5
.= (power L) . (x,n0) by A2, A4, Th28 ;
thus  eval (((<%(0. L),(1. L)%> `^ n0) - (1_. L)),x) = (eval ((<%(0. L),(1. L)%> `^ n0),x)) - (eval ((1_. L),x)) by POLYNOM4:21
.= (eval ((<%(0. L),(1. L)%> `^ n0),x)) - (1. L) by POLYNOM4:18
.= ((power L) . ((eval (<%(0. L),(1. L)%>,x)),n0)) - (1. L) by POLYNOM5:22
.= xn - (1_ (INT.Ring p)) by A2, A6, POLYNOM5:48 ; ::_thesis: verum
end;
A7: len (1_. L) = 1 by POLYNOM4:4;
 len <%(0. L),(1. L)%> = 2 by POLYNOM5:40;
then A8: len (<%(0. L),(1. L)%> `^ n0) = ((n * 2) - n) + 1 by POLYNOM5:23
.= n + 1 ;
A9: 0 + 1 < n + 1 by A1, XREAL_1:8;
then  len (<%(0. L),(1. L)%> `^ n0) <> len (- (1_. L)) by A8, A7, POLYNOM4:8;
then  len ((<%(0. L),(1. L)%> `^ n0) - (1_. L)) = max ((len (<%(0. L),(1. L)%> `^ n0)),(len (- (1_. L)))) by POLYNOM4:7
.= max ((n + 1),1) by A8, A7, POLYNOM4:8
.= n + 1 by A9, XXREAL_0:def_10 ;
then  deg ((<%(0. L),(1. L)%> `^ n0) - (1_. L)) = n ;
hence  ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) ) by A3; ::_thesis: verum
end;

theorem Th29: :: INT_7:29
for p being Prime
for a, b being Element of (Z/Z* p)
for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
proof
let p be Prime; ::_thesis: for a, b being Element of (Z/Z* p)
for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
let a, b be Element of (Z/Z* p); ::_thesis: for n being Nat st 0 < n & ord a = n & b |^ n = 1 holds
b is Element of (gr {a})
let n be Nat; ::_thesis: ( 0 < n & ord a = n & b |^ n = 1 implies b is Element of (gr {a}) )
assume that
A1: 0 < n and
A2: ord a = n and
A3: b |^ n = 1 ; ::_thesis: b is Element of (gr {a})
reconsider XX = the carrier of (gr {a}) as finite set ;
A4: ex D being finite set st
( D = the carrier of (gr {a}) & card (gr {a}) = card D ) ;
reconsider L = INT.Ring p as non empty unital doubleLoopStr ;
consider f being Polynomial of L such that
A5: deg f = n and
A6: for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) by A1, Lm14;
consider m, n0 being Element of NAT  such that
A7: n0 = deg f and
A8: m = card (Roots f) and
A9: m <= n0 by A5, Th27;
assume  b is not Element of (gr {a}) ; ::_thesis: contradiction
then  card ( the carrier of (gr {a}) \/ {b}) = (card XX) + 1 by CARD_2:41
.= n0 + 1 by A2, A5, A7, A4, GR_CY_1:7 ;
then A10: card (n0 + 1) = card ( the carrier of (gr {a}) \/ {b}) ;
A11: 1 < p by INT_2:def_4;
A12: for x being Element of (Z/Z* p) st x |^ n = 1 holds
x in Roots f
proof
let x1 be Element of (Z/Z* p); ::_thesis: ( x1 |^ n = 1 implies x1 in Roots f )
assume  x1 |^ n = 1 ; ::_thesis: x1 in Roots f
then A13: x1 |^ n = 1_ (Z/Z* p) by Th21
.= 1_ (INT.Ring p) by Th21 ;
 x1 |^ n in Segm0 p ;
then  x1 |^ n in (Segm p) \ {0} by A11, Def2;
then reconsider x2 = x1 |^ n as Element of (INT.Ring p) by XBOOLE_0:def_5;
 x1 in Segm0 p ;
then  x1 in (Segm p) \ {0} by A11, Def2;
then reconsider x3 = x1 as Element of L by XBOOLE_0:def_5;
eval (f,x3) = x2 - (1_ (INT.Ring p)) by A6
.= 0. L by A13, RLVECT_1:15 ;
then  x3 is_a_root_of f by POLYNOM5:def_6;
hence  x1 in Roots f by POLYNOM5:def_9; ::_thesis: verum
end;
A14: the carrier of (gr {a}) c= Roots f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (gr {a}) or x in Roots f )
assume A15: x in the carrier of (gr {a}) ; ::_thesis: x in Roots f
then  x in gr {a} by STRUCT_0:def_5;
then  x in Z/Z* p by GROUP_2:40;
then reconsider x1 = x as Element of (Z/Z* p) by STRUCT_0:def_5;
 x1 in gr {a} by A15, STRUCT_0:def_5;
then consider j being Integer such that
A16: x1 = a |^ j by GR_CY_1:5;
x1 |^ n = a |^ (j * n) by A16, GROUP_1:35
.= (a |^ n) |^ j by GROUP_1:35
.= (1_ (Z/Z* p)) |^ j by A2, GROUP_1:41
.= 1_ (Z/Z* p) by GROUP_1:31
.= 1 by Th21 ;
hence  x in Roots f by A12; ::_thesis: verum
end;
 b in Roots f by A3, A12;
then  {b} c= Roots f by ZFMISC_1:31;
then  the carrier of (gr {a}) \/ {b} c= Roots f by A14, XBOOLE_1:8;
then A17: card ( the carrier of (gr {a}) \/ {b}) c= card (Roots f) by CARD_1:11;
 card m = card (Roots f) by A8;
then  n0 + 1 c= m by A17, A10, CARD_1:41;
then  n0 + 1 <= m by NAT_1:39;
hence  contradiction by A9, NAT_1:16, XXREAL_0:2; ::_thesis: verum
end;

theorem Th30: :: INT_7:30
for G being Group
for z being Element of G
for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l
proof
let G be Group; ::_thesis: for z being Element of G
for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l
let z be Element of G; ::_thesis: for d, l being Element of NAT st G is finite & ord z = d * l holds
ord (z |^ d) = l
let d, l be Element of NAT ; ::_thesis: ( G is finite & ord z = d * l implies ord (z |^ d) = l )
assume that
A1: G is finite and
A2: ord z = d * l ; ::_thesis: ord (z |^ d) = l
set m = d * l;
reconsider H = gr {z} as strict Subgroup of G ;
reconsider H = H as finite strict Subgroup of G by A1;
 z in gr {z} by GR_CY_2:2;
then reconsider z1 = z as Element of H by STRUCT_0:def_5;
A3: gr {z} = gr {z1} by GR_CY_2:3;
 card H = d * l by A1, A2, GR_CY_1:7;
then  ord (z1 |^ d) = l by A3, GR_CY_2:8;
hence  ord (z |^ d) = l by A1, GROUP_8:3, GROUP_8:5; ::_thesis: verum
end;

theorem :: INT_7:31
for p being Prime holds Z/Z* p is cyclic Group
proof
let p be Prime; ::_thesis: Z/Z* p is cyclic Group
set a = the Element of (Z/Z* p);
set ZP = Z/Z* p;
defpred S1[ Nat, Element of (Z/Z* p), Element of (Z/Z* p)] means  ord $2 < ord $3;
assume A1: Z/Z* p is not cyclic Group ; ::_thesis: contradiction
A2: for x being Element of (Z/Z* p) holds ord x < card (Z/Z* p)
proof
let x be Element of (Z/Z* p); ::_thesis: ord x < card (Z/Z* p)
A3: ord x <= card (Z/Z* p) by GR_CY_1:8, NAT_D:7;
 ord x <> card (Z/Z* p) by A1, GR_CY_1:19;
hence  ord x < card (Z/Z* p) by A3, XXREAL_0:1; ::_thesis: verum
end;
A4: for n being Element of NAT
for x being Element of (Z/Z* p) ex y being Element of (Z/Z* p) st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of (Z/Z* p) ex y being Element of (Z/Z* p) st S1[n,x,y]
let x be Element of (Z/Z* p); ::_thesis: ex y being Element of (Z/Z* p) st S1[n,x,y]
set n = ord x;
 ord x < card (Z/Z* p) by A2;
then A5: card (gr {x}) <> card (Z/Z* p) by GR_CY_1:7;
 the carrier of (gr {x}) c= the carrier of (Z/Z* p) by GROUP_2:def_5;
then  the carrier of (gr {x}) c< the carrier of (Z/Z* p) by A5, XBOOLE_0:def_8;
then  the carrier of (Z/Z* p) \ the carrier of (gr {x}) <> {} by XBOOLE_1:105;
then consider z being set  such that
A6: z in the carrier of (Z/Z* p) \ the carrier of (gr {x}) by XBOOLE_0:def_1;
reconsider z = z as Element of (Z/Z* p) by A6;
set m = ord z;
now__::_thesis:_ex_y_being_Element_of_the_carrier_of_(Z/Z*_p)_st_ord_x_<_ord_y
set l = (ord z) lcm (ord x);
 1 <= card (gr {x}) by GROUP_1:45;
then A7: 1 <= ord x by GR_CY_1:7;
 not ord z divides ord x
proof
assume  ord z divides ord x ; ::_thesis: contradiction
then consider j being Integer such that
A8: ord x = (ord z) * j by INT_1:def_3;
z |^ (ord x) = (z |^ (ord z)) |^ j by A8, GROUP_1:35
.= (1_ (Z/Z* p)) |^ j by GROUP_1:41
.= 1_ (Z/Z* p) by GROUP_1:31
.= 1 by Th21 ;
then  z is Element of (gr {x}) by A7, Th29;
hence  contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
then A9: ord x <> (ord z) lcm (ord x) by INT_2:18;
 1 <= card (gr {z}) by GROUP_1:45;
then A10: 1 <= ord z by GR_CY_1:7;
then consider m0, n0 being Element of NAT  such that
A11: (ord z) lcm (ord x) = n0 * m0 and
A12: n0 gcd m0 = 1 and
A13: n0 divides ord x and
A14: m0 divides ord z and
A15: n0 <> 0 and
A16: m0 <> 0 by A7, Th17;
consider j being Integer such that
A17: ord x = n0 * j by A13, INT_1:def_3;
consider u being Integer such that
A18: ord z = m0 * u by A14, INT_1:def_3;
 (ord z) / m0 = u by A16, A18, XCMPLX_1:89;
then reconsider d2 = (ord z) / m0 as Element of NAT by INT_1:3;
 ord z = ((ord z) / m0) * m0 by A16, XCMPLX_1:87;
then A19: ord (z |^ d2) = m0 by Th30;
 (ord x) / n0 = j by A15, A17, XCMPLX_1:89;
then reconsider d1 = (ord x) / n0 as Element of NAT by INT_1:3;
 ord x divides (ord z) lcm (ord x) by INT_2:18;
then consider j being Integer such that
A20: (ord z) lcm (ord x) = (ord x) * j by INT_1:def_3;
take y = (x |^ d1) * (z |^ d2); ::_thesis: ord x < ord y
 ord x = ((ord x) / n0) * n0 by A15, XCMPLX_1:87;
then  ord (x |^ d1) = n0 by Th30;
then A21: ord y = m0 * n0 by A12, A19, Th25;
 ((ord z) lcm (ord x)) / (ord x) = j by A7, A20, XCMPLX_1:89;
then A22: j is Element of NAT by INT_1:3;
 j <> 0 by A7, A10, A20, INT_2:4;
then  (ord x) * 1 <= (ord x) * j by A22, NAT_1:14, XREAL_1:64;
hence  ord x < ord y by A11, A21, A9, A20, XXREAL_0:1; ::_thesis: verum
end;
hence  ex y being Element of (Z/Z* p) st S1[n,x,y] ; ::_thesis: verum
end;
consider f being Function of NAT, the carrier of (Z/Z* p) such that
A23: ( f . 0 = the Element of (Z/Z* p) & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A4);
deffunc H1( Element of NAT ) ->  Element of NAT = ord (f . $1);
consider g being Function of NAT,NAT such that
A24: for k being Element of NAT holds g . k = H1(k) from FUNCT_2:sch_4();
A25: now__::_thesis:_for_k_being_Element_of_NAT_holds_g_._k_<_g_._(k_+_1)
let k be Element of NAT ; ::_thesis: g . k < g . (k + 1)
A26: g . (k + 1) = ord (f . (k + 1)) by A24;
 g . k = ord (f . k) by A24;
hence  g . k < g . (k + 1) by A23, A26; ::_thesis: verum
end;
A27: for k, m being Element of NAT holds g . k < g . ((k + 1) + m)
proof
let k be Element of NAT ; ::_thesis: for m being Element of NAT holds g . k < g . ((k + 1) + m)
defpred S2[ Nat] means g . k < g . ((k + 1) + $1);
A28: now__::_thesis:_for_m_being_Element_of_NAT_st_S2[m]_holds_
S2[m_+_1]
let m be Element of NAT ; ::_thesis: ( S2[m] implies S2[m + 1] )
assume A29: S2[m] ; ::_thesis: S2[m + 1]
 g . ((k + 1) + m) < g . (((k + 1) + m) + 1) by A25;
hence  S2[m + 1] by A29, XXREAL_0:2; ::_thesis: verum
end;
A30: S2[ 0 ] by A25;
 for m being Element of NAT holds S2[m] from NAT_1:sch_1(A30, A28);
hence  for m being Element of NAT holds g . k < g . ((k + 1) + m) ; ::_thesis: verum
end;
A31: for k, m being Element of NAT st k < m holds
g . k < g . m
proof
let k, m be Element of NAT ; ::_thesis: ( k < m implies g . k < g . m )
assume A32: k < m ; ::_thesis: g . k < g . m
then  m - k is Element of NAT by INT_1:5;
then reconsider mk = m - k as Nat ;
 m - k <> 0 by A32;
then consider n0 being Nat such that
A33: mk = n0 + 1 by NAT_1:6;
reconsider n = n0 as Element of NAT by ORDINAL1:def_12;
 m = (k + 1) + n by A33;
hence  g . k < g . m by A27; ::_thesis: verum
end;
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_NAT_&_x2_in_NAT_&_g_._x1_=_g_._x2_holds_
x2_=_x1
let x1, x2 be set ; ::_thesis: ( x1 in NAT & x2 in NAT & g . x1 = g . x2 implies x2 = x1 )
assume that
A34: x1 in NAT and
A35: x2 in NAT and
A36: g . x1 = g . x2 ; ::_thesis: x2 = x1
reconsider xx1 = x1, xx2 = x2 as Element of NAT by A34, A35;
A37: xx2 <= xx1 by A31, A36;
 xx1 <= xx2 by A31, A36;
hence  x2 = x1 by A37, XXREAL_0:1; ::_thesis: verum
end;
then  g is one-to-one by FUNCT_2:19;
then  dom g, rng g are_equipotent by WELLORD2:def_4;
then  card (dom g) = card (rng g) by CARD_1:5;
then A38: card (rng g) = card NAT by FUNCT_2:def_1;
 rng g c= Segm (card (Z/Z* p))
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng g or y in Segm (card (Z/Z* p)) )
assume  y in rng g ; ::_thesis: y in Segm (card (Z/Z* p))
then consider x being set  such that
A39: x in NAT and
A40: y = g . x by FUNCT_2:11;
reconsider x = x as Element of NAT by A39;
reconsider gg = g . x as Element of NAT ;
 g . x = ord (f . x) by A24;
then  gg < card (Z/Z* p) by A2;
hence  y in Segm (card (Z/Z* p)) by A40, ALGSEQ_1:1; ::_thesis: verum
end;
hence  contradiction by A38; ::_thesis: verum
end;