let p be FinSequence of NAT ; :: thesis: for x being Element of NAT
for b being bag of 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 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 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 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 ; :: 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 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 A1: ( b is prime-factorization-like & 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 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)) )
p = (b * (canFS (support b))) | (dom p) by A1, FINSEQ_1:33;
then A2: dom p = (dom (b * (canFS (support b)))) /\ (dom p) by RELAT_1:90;
A3: rng (canFS (support b)) = support b by FUNCT_2:def 3;
dom b = SetPrimes by PARTFUN1:def 4;
then A4: dom (b * (canFS (support b))) = dom (canFS (support b)) by A3, RELAT_1:46;
A5: rng (canFS (support b)) = support b by FUNCT_2:def 3;
A6: len <*x*> = 1 by FINSEQ_1:57;
then A7: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:35;
(len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:6;
then A8: (len p) + 1 in dom (b * (canFS (support b))) by A1, A7, FINSEQ_1:def 3;
A9: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:59
.= b . ((canFS (support b)) . ((len p) + 1)) by A1, A4, A8, FUNCT_1:23 ;
A10: (canFS (support b)) . ((len p) + 1) in support b by A4, A5, A8, FUNCT_1:12;
then reconsider q = (canFS (support b)) . ((len p) + 1) as Prime by NEWTON:def 6;
consider n being natural number such that
A11: ( 0 < n & b . q = q |^ n ) by A1, A10, Def1;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ set ] means $1 in (support b) \ {q};
deffunc H₁( set ) -> Element of NAT = b . $1;
deffunc H₂( set ) -> Element of NAT = 0 ;
consider b1 being ManySortedSet of such that
A12: for i being Element of SetPrimes st i in SetPrimes holds
( ( S₁[i] implies b1 . i = H₁(i) ) & ( not S₁[i] implies b1 . i = H₂(i) ) ) from PRE_CIRC:sch 2();
A13: support b1 = (support b) \ {q}

proof

now

let z be set ; :: thesis: ( z in support b1 implies z in (support b) \ {q} )
assume A14: 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 4;
hence contradiction by A14, POLYNOM1:def 7; :: thesis: verum

end;

then reconsider y = z as Element of SetPrimes by PARTFUN1:def 4;
A15: b1 . y <> 0 by A14, POLYNOM1:def 7;
assume not z in (support b) \ {q} ; :: thesis: contradiction
hence contradiction by A12, A15; :: thesis: verum

end;

then A16: support b1 c= (support b) \ {q} by TARSKI:def 3;

now

let z be set ; :: thesis: ( z in (support b) \ {q} implies z in support b1 )
assume A17: z in (support b) \ {q} ; :: thesis: z in support b1
then A18: z in support b by XBOOLE_0:def 5;
reconsider y = z as Element of SetPrimes by A17;
b1 . y = b . y by A12, A17;
then b1 . y <> 0 by A18, POLYNOM1:def 7;
hence z in support b1 by POLYNOM1:def 7; :: thesis: verum

end;

then (support b) \ {q} c= support b1 by TARSKI:def 3;
hence support b1 = (support b) \ {q} by A16, XBOOLE_0:def 10; :: thesis: verum

end;

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
A19: ( x in dom b1 & y = b1 . x ) by FUNCT_1:def 5;
reconsider x = x as Element of SetPrimes by A19, PARTFUN1:def 4;
b1 . x in NAT

proof

per cases ( 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 A12;
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 A12;
hence b1 . x in NAT ; :: thesis: verum

end;

end;

end;

hence y in NAT by A19; :: thesis: verum

end;

then reconsider b1 = b1 as bag of by A13, POLYNOM1:def 8, VALUED_0:def 6;

A20: now

let x be Prime; :: thesis: ( x in support b1 implies ex m being natural number st
( 0 < m & b1 . x = x |^ m ) )
assume A21: x in support b1 ; :: thesis: ex m being natural number st
( 0 < m & b1 . x = x |^ m )
(support b) \ {q} c= support b by XBOOLE_1:36;
then consider m being natural number such that
A22: ( 0 < m & b . x = x |^ m ) by A1, A13, A21, Def1;
take m = m; :: thesis: ( 0 < m & b1 . x = x |^ m )
thus 0 < m by A22; :: thesis: b1 . x = x |^ m
thus b1 . x = x |^ m by A12, A13, A21, A22; :: thesis: verum

end;

dom b = SetPrimes by PARTFUN1:def 4;
then dom (b * (canFS (support b))) = dom (canFS (support b)) by A3, RELAT_1:46;
then A23: dom ((canFS (support b)) | (dom p)) = dom p by A2, RELAT_1:91, XBOOLE_1:17;
A24: SetPrimes = dom b by PARTFUN1:def 4;
A25: rng (canFS (support b)) = support b by FUNCT_2:def 3;
A26: card (dom (b * (canFS (support b)))) = card (dom (canFS (support b))) by A24, A25, RELAT_1:46
.= card (Seg (len (canFS (support b)))) by FINSEQ_1:def 3
.= card (len (canFS (support b))) by FINSEQ_1:76
.= len (canFS (support b)) ;
A27: len (canFS (support b)) = card (Seg (len (p ^ <*x*>))) by A1, A26, FINSEQ_1:def 3
.= card (len (p ^ <*x*>)) by FINSEQ_1:76
.= (len p) + 1 by A6, FINSEQ_1:35 ;
A28: dom (canFS (support b1)) = dom p

proof

A29: card ((support b) \ {q}) = (card (support b)) - (card {q}) by A4, A5, A8, EULER_1:5, FUNCT_1:12
.= (card (support b)) - 1 by CARD_1:50 ;
A30: card (support b) = len (canFS (support b)) by UPROOTS:5;
len (canFS (support b1)) = len p by A13, A27, A29, A30, UPROOTS:5;
then dom (canFS (support b1)) = Seg (len p) by FINSEQ_1:def 3;
hence dom (canFS (support b1)) = dom p by FINSEQ_1:def 3; :: thesis: verum

end;

per cases ( dom p = {} or dom p <> {} ) ;

suppose A31: dom p = {} ; :: thesis: ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of 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));
A32: p = {} by A31;
Seg (len (canFS (support b1))) = dom (canFS (support b1)) by FINSEQ_1:def 3
.= Seg (len p) by A28, FINSEQ_1:def 3
.= Seg 0 by A32 ;
then len (canFS (support b1)) = 0 ;
then canFS (support b1) = {} ;
then A33: b1 * (canFS (support b1)) = <*> NAT ;
reconsider p1 = b1 * (canFS (support b1)) as FinSequence of NAT by A33;
take p1 ; :: thesis: ex q being Prime ex n being Element of NAT ex b1 being bag of 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 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 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 A4, A5, A8, A9, A11, A13, A20, A31, A33, Def1, FUNCT_1:12, RELAT_1:64; :: thesis: verum

end;

suppose A34: dom p <> {} ; :: thesis: ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of 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)) )

A35: (support b) \ {q} <> {}

proof

assume (support b) \ {q} = {} ; :: thesis: contradiction
then A36: rng (canFS (support b1)) = {} by A13;
dom p = {}

proof

assume dom p <> {} ; :: thesis: contradiction
then consider x being set such that
A37: x in dom p by XBOOLE_0:def 1;
thus contradiction by A28, A36, A37, FUNCT_1:12; :: thesis: verum

end;

hence contradiction by A34; :: thesis: verum

end;

A38: rng ((canFS (support b)) | (dom p)) = (support b) \ {q}

proof

now

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
A39: ( x in dom ((canFS (support b)) | (dom p)) & y = ((canFS (support b)) | (dom p)) . x ) by FUNCT_1:def 5;
A40: y = (canFS (support b)) . x by A39, FUNCT_1:70;
A41: x in (dom (canFS (support b))) /\ (dom p) by A39, RELAT_1:90;
then A42: x in dom (canFS (support b)) by XBOOLE_0:def 4;
A43: x in dom p by A41, XBOOLE_0:def 4;
A44: y in rng (canFS (support b)) by A40, A42, FUNCT_1:12;
y <> q

proof

assume A46: y = q ; :: thesis: contradiction
(len p) + 1 in Seg ((len p) + 1) by FINSEQ_1:6;
then (len p) + 1 in dom (canFS (support b)) by A27, FINSEQ_1:def 3;
then (len p) + 1 = x by A40, A42, A46, FUNCT_1:def 8;
then A47: (len p) + 1 in Seg (len p) by A43, FINSEQ_1:def 3;
(len p) + 0 < 1 + (len p) by XREAL_1:10;
hence contradiction by A47, FINSEQ_1:3; :: thesis: verum

end;

then not y in {q} by TARSKI:def 1;
hence y in (support b) \ {q} by A44, XBOOLE_0:def 5; :: thesis: verum

end;

then A48: rng ((canFS (support b)) | (dom p)) c= (support b) \ {q} by TARSKI:def 3;
A49: rng (canFS (support b)) = support b by FUNCT_2:def 3;

now

let y be set ; :: thesis: ( y in (support b) \ {q} implies y in rng ((canFS (support b)) | (dom p)) )
assume A50: y in (support b) \ {q} ; :: thesis: y in rng ((canFS (support b)) | (dom p))
then y in rng (canFS (support b)) by A49, XBOOLE_0:def 5;
then consider x being set such that
A51: ( x in dom (canFS (support b)) & y = (canFS (support b)) . x ) by FUNCT_1:def 5;
A52: x in dom p

proof

assume not x in dom p ; :: thesis: contradiction
then A53: not x in Seg (len p) by FINSEQ_1:def 3;
A54: x in Seg ((len p) + 1) by A27, A51, FINSEQ_1:def 3;
reconsider x = x as Element of NAT by A51;
A55: ( 1 <= x & x <= (len p) + 1 ) by A54, FINSEQ_1:3;
len p < x by A53, A55;
then (len p) + 1 <= x by NAT_1:13;
then x = (len p) + 1 by A55, XXREAL_0:1;
then y in {q} by A51, TARSKI:def 1;
hence contradiction by A50, XBOOLE_0:def 5; :: thesis: verum

end;

then A56: y = ((canFS (support b)) | (dom p)) . x by A51, FUNCT_1:72;
x in (dom (canFS (support b))) /\ (dom p) by A51, A52, XBOOLE_0:def 4;
then x in dom ((canFS (support b)) | (dom p)) by RELAT_1:90;
hence y in rng ((canFS (support b)) | (dom p)) by A56, FUNCT_1:12; :: thesis: verum

end;

then (support b) \ {q} c= rng ((canFS (support b)) | (dom p)) by TARSKI:def 3;
hence rng ((canFS (support b)) | (dom p)) = (support b) \ {q} by A48, XBOOLE_0:def 10; :: thesis: verum

end;

reconsider L0 = (canFS (support b)) | (dom p) as Function of (dom p),((support b) \ {q}) by A23, A38, FUNCT_2:3;
A57: ( rng L0 = (support b) \ {q} & dom L0 = dom p ) by A35, A38, FUNCT_2:def 1;
A60: L0 is one-to-one by FUNCT_1:84;
then L0 " is one-to-one ;
then A61: (L0 " ) * (canFS (support b1)) is one-to-one ;
L0 is one-to-one by FUNCT_1:84;
then A62: ( dom (L0 " ) = (support b) \ {q} & rng (L0 " ) = dom p ) by A57, FUNCT_1:55;
then reconsider LL1 = L0 " as Function of ((support b) \ {q}),(dom p) by FUNCT_2:3;
A63: rng (canFS (support b1)) = support b1 by FUNCT_2:def 3;
canFS (support b1) is Function of (dom p),((support b) \ {q}) by A13, A28, A63, FUNCT_2:3;
then reconsider L0L = LL1 * (canFS (support b1)) as Function of (dom p),(dom p) by A35, FUNCT_2:19;
rng L0L = dom p by A13, A62, A63, RELAT_1:47;
then L0L is onto by FUNCT_2:def 3;
then reconsider LL = L0L as Permutation of (dom p) by A61;
((canFS (support b)) | (dom p)) * LL = (((canFS (support b)) | (dom p)) * LL1) * (canFS (support b1)) by RELAT_1:55
.= (id (support b1)) * (canFS (support b1)) by A13, A35, A38, A60, FUNCT_2:35
.= canFS (support b1) by FUNCT_2:23 ;
then A64: (canFS (support b1)) * (LL " ) = ((canFS (support b)) | (dom p)) * (LL * (LL " )) by RELAT_1:55;
rng LL = dom p by FUNCT_2:def 3;
then A65: (canFS (support b1)) * (LL " ) = ((canFS (support b)) | (dom p)) * (id (dom p)) by A34, A64, FUNCT_2:35;
reconsider L = LL " as Permutation of (dom p) ;
reconsider FS = canFS (support b1) as FinSequence ;
A66: rng L = dom FS by A28, FUNCT_2:def 3;
then A67: dom (FS * L) = dom L by RELAT_1:46
.= dom p by A34, FUNCT_2:def 1 ;
A68: SetPrimes = dom b1 by PARTFUN1:def 4;
rng (canFS (support b1)) = support b1 by FUNCT_2:def 3;
then A69: dom (b1 * FS) = dom p by A28, A68, RELAT_1:46;
A70: rng (FS * L) = rng FS by A66, RELAT_1:47
.= (support b) \ {q} by A13, FUNCT_2:def 3 ;
SetPrimes = dom b1 by PARTFUN1:def 4;
then A71: dom p = dom (b1 * (FS * L)) by A67, A70, RELAT_1:46;

A72: now

let k be set ; :: thesis: ( k in dom p implies p . k = (b1 * (FS * L)) . k )
assume A73: k in dom p ; :: thesis: p . k = (b1 * (FS * L)) . k
A74: dom p c= dom (p ^ <*x*>) by FINSEQ_1:39;
A76: (FS * L) . k in (support b) \ {q} by A67, A70, A73, FUNCT_1:12;
thus p . k = (p ^ <*x*>) . k by A73, FINSEQ_1:def 7
.= b . ((canFS (support b)) . k) by A1, A73, A74, FUNCT_1:22
.= b . (((canFS (support b)) | (dom p)) . k) by A73, FUNCT_1:72
.= b . ((FS * L) . k) by A65, FUNCT_2:23
.= b1 . ((FS * L) . k) by A12, A76
.= (b1 * (FS * L)) . k by A71, A73, FUNCT_1:22 ; :: thesis: verum

end;

set p1 = b1 * FS;
A77: p = b1 * (FS * L) by A71, A72, FUNCT_1:9
.= (b1 * FS) * L by RELAT_1:55 ;
A78: p,b1 * FS are_fiberwise_equipotent by A69, A77, CLASSES1:88;
dom (b1 * FS) = Seg (len p) by A69, FINSEQ_1:def 3;
then A79: b1 * FS is FinSequence by FINSEQ_1:def 2;
rng (b1 * FS) c= NAT by VALUED_0:def 6;
then reconsider p1 = b1 * FS as FinSequence of NAT by A79, FINSEQ_1:def 4;
A80: Seg (len p1) = dom p by A69, FINSEQ_1:def 3;
take p1 ; :: thesis: ex q being Prime ex n being Element of NAT ex b1 being bag of 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 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 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 A4, A5, A8, A9, A11, A13, A20, A78, A80, Def1, EULER_2:25, FINSEQ_1:def 3, FUNCT_1:12; :: thesis: verum

end;

end;