deffunc H₁( 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 H₂( set ) -> Element of NAT = b . $1;
A6: card (support b) = len (canFS (support b)) by FINSEQ_1:93;
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 S₁[ 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
( ( S₁[i] implies b1 . i = H₂(i) ) & ( not S₁[i] implies b1 . i = H₁(i) ) ) from PRE_CIRC:sch 2();
A15: rng b1 c= NAT

proof

let y be object ; :: 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 object 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

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 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 object st z in support b1 holds
z in (support b) \ {q}

let z be object ; :: 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} ;

now :: thesis: for z being object st z in (support b) \ {q} holds
z in support b1

let z be object ; :: 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 ;
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;
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, FINSEQ_1:93;
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;
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;

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

suppose A36: 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, FUNCT_1:3, RELAT_1:41, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A39: 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 object st y in (support b) \ {q} holds
y in rng ((canFS (support b)) | (dom p))

let y be object ; :: 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 object 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)) ;

now :: thesis: for y being object st y in rng ((canFS (support b)) | (dom p)) holds
y in (support b) \ {q}

let y be object ; :: 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 object 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} ;
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 object st k in dom p holds
p . k = (b1 * (FS * L)) . k

let k be object ; :: 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 ;
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, EULER_2:10, FINSEQ_1:def 3, FUNCT_1:3, XBOOLE_0:def 10; :: thesis: verum

end;

end;