:: WSIERP_1 semantic presentation

begin


theorem Th1: :: WSIERP_1:1
for x being real number holds
( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
proof
let x be real number ; ::_thesis: ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 )
A1: (- x) |^ 1 = - x by NEWTON:5;
A2: x = x |^ 1 by NEWTON:5;
then  x |^ (1 + 1) = x * x by NEWTON:8;
then x |^ 2 = (- x) * (- x)
.= (- x) |^ (1 + 1) by A1, NEWTON:8 ;
hence  ( x |^ 2 = x * x & (- x) |^ 2 = x |^ 2 ) by A2, NEWTON:8; ::_thesis: verum
end;

theorem Th2: :: WSIERP_1:2
for x being real number
for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
proof
let x be real number ; ::_thesis: for a being Nat holds
( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
let a be Nat; ::_thesis: ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) )
A1: (- x) |^ (2 * a) = ((- x) |^ 2) |^ a by NEWTON:9
.= (x |^ 2) |^ a by Th1
.= x |^ (2 * a) by NEWTON:9 ;
(- x) |^ ((2 * a) + 1) = ((- x) |^ (2 * a)) * (- x) by NEWTON:6
.= - ((x |^ (2 * a)) * x) by A1
.= - (x |^ ((2 * a) + 1)) by NEWTON:6 ;
hence  ( (- x) |^ (2 * a) = x |^ (2 * a) & (- x) |^ ((2 * a) + 1) = - (x |^ ((2 * a) + 1)) ) by A1; ::_thesis: verum
end;

theorem Th3: :: WSIERP_1:3
for x, y being real number
for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
proof
let x, y be real number ; ::_thesis: for d being Nat st x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d holds
x = y
let d be Nat; ::_thesis: ( x >= 0 & y >= 0 & d > 0 & x |^ d = y |^ d implies x = y )
assume that
A1: x >= 0 and
A2: y >= 0 and
A3: d > 0 and
A4: x |^ d = y |^ d ; ::_thesis: x = y
A5: d >= 1 by A3, NAT_1:14;
then x = d -Root (x |^ d) by A1, PREPOWER:19
.= y by A2, A4, A5, PREPOWER:19 ;
hence  x = y ; ::_thesis: verum
end;

Lm1:  for x, y being real number holds
( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
proof
let x, y be real number ; ::_thesis: ( ( x >= 0 implies x + y >= y ) & ( x + y >= y implies x >= 0 ) & ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
A1: ( x >= 0 iff x + y >= 0 + y ) by XREAL_1:6;
hence  ( x >= 0 iff x + y >= y ) ; ::_thesis: ( ( x > 0 implies x + y > y ) & ( x + y > y implies x > 0 ) & ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
A2: ( x > 0 iff x + y > 0 + y ) by XREAL_1:6;
hence  ( x > 0 iff x + y > y ) ; ::_thesis: ( ( x >= 0 implies y >= y - x ) & ( y >= y - x implies x >= 0 ) & ( x > 0 implies y > y - x ) & ( y > y - x implies x > 0 ) )
thus  ( x >= 0 iff y >= y - x ) by A1, XREAL_1:20; ::_thesis: ( x > 0 iff y > y - x )
thus  ( x > 0 iff y > y - x ) by A2, XREAL_1:19; ::_thesis: verum
end;

Lm2:  for x, y, z being real number st x >= 0 & y >= z holds
( x + y >= z & y >= z - x )
proof
let x, y, z be real number ; ::_thesis: ( x >= 0 & y >= z implies ( x + y >= z & y >= z - x ) )
assume  ( x >= 0 & y >= z ) ; ::_thesis: ( x + y >= z & y >= z - x )
then  x + y >= z + 0 by XREAL_1:7;
hence  ( x + y >= z & y >= z - x ) by XREAL_1:20; ::_thesis: verum
end;

Lm3:  for x, y, z being real number st ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) holds
( x + y > z & y > z - x )
proof
let x, y, z be real number ; ::_thesis: ( ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) implies ( x + y > z & y > z - x ) )
assume  ( ( x >= 0 & y > z ) or ( x > 0 & y >= z ) ) ; ::_thesis: ( x + y > z & y > z - x )
then  x + y > z + 0 by XREAL_1:8;
hence  ( x + y > z & y > z - x ) by XREAL_1:19; ::_thesis: verum
end;

registration
let k be Integer;
let a be Nat;
clusterk |^ a ->  integer ;
coherence
 k |^ a is integer
proof
defpred S1[ Nat] means k |^ k is Integer;
A1: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] )
assume  k |^ a is Integer ; ::_thesis: S1[a + 1]
then reconsider b = k |^ a as Integer ;
 k |^ (a + 1) = k * b by NEWTON:6;
hence  S1[a + 1] ; ::_thesis: verum
end;
A2: S1[ 0 ] by NEWTON:4;
 for a being Nat holds S1[a] from NAT_1:sch_2(A2, A1);
hence  k |^ a is integer ; ::_thesis: verum
end;
end;

Lm4:  for a being Nat ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
proof
let a be Nat; ::_thesis: ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 )
set b = a div 2;
set d = a mod 2;
 a = (2 * (a div 2)) + (a mod 2) by NAT_D:2;
then  ( a = (2 * (a div 2)) + 0 or a = (2 * (a div 2)) + 1 ) by NAT_1:23, NAT_D:1;
hence  ex b being Nat st
( a = 2 * b or a = (2 * b) + 1 ) ; ::_thesis: verum
end;

theorem Th4: :: WSIERP_1:4
for k, m, n being Integer st k divides m & k divides n holds
k divides m + n
proof
let k, m, n be Integer; ::_thesis: ( k divides m & k divides n implies k divides m + n )
assume that
A1: k divides m and
A2: k divides n ; ::_thesis: k divides m + n
consider m1 being Integer such that
A3: m = k * m1 by A1, INT_1:def_3;
consider n1 being Integer such that
A4: n = k * n1 by A2, INT_1:def_3;
 m + n = k * (m1 + n1) by A3, A4;
hence  k divides m + n by INT_1:def_3; ::_thesis: verum
end;

theorem Th5: :: WSIERP_1:5
for k, m, n, m1, n1 being Integer st k divides m & k divides n holds
k divides (m * m1) + (n * n1)
proof
let k, m, n, m1, n1 be Integer; ::_thesis: ( k divides m & k divides n implies k divides (m * m1) + (n * n1) )
assume  ( k divides m & k divides n ) ; ::_thesis: k divides (m * m1) + (n * n1)
then  ( k divides m * m1 & k divides n * n1 ) by INT_2:2;
hence  k divides (m * m1) + (n * n1) by Th4; ::_thesis: verum
end;

theorem Th6: :: WSIERP_1:6
for m, n, k being Integer st m gcd n = 1 & k gcd n = 1 holds
(m * k) gcd n = 1
proof
let m, n, k be Integer; ::_thesis: ( m gcd n = 1 & k gcd n = 1 implies (m * k) gcd n = 1 )
assume  ( m gcd n = 1 & k gcd n = 1 ) ; ::_thesis: (m * k) gcd n = 1
then  ( m,n are_relative_prime & k,n are_relative_prime ) by INT_2:def_3;
then  m * k,n are_relative_prime by INT_2:26;
hence  (m * k) gcd n = 1 by INT_2:def_3; ::_thesis: verum
end;

theorem :: WSIERP_1:7
for a, b, c being Nat st a gcd b = 1 & c gcd b = 1 holds
(a * c) gcd b = 1 by Th6;

theorem Th8: :: WSIERP_1:8
for m being Integer holds
( 0 gcd m = abs m & 1 gcd m = 1 )
proof
let m be Integer; ::_thesis: ( 0 gcd m = abs m & 1 gcd m = 1 )
A1: m gcd 1 = (abs m) gcd (abs 1) by INT_2:34
.= (abs m) gcd 1 by ABSVALUE:def_1
.= 1 by NEWTON:51 ;
m gcd 0 = (abs m) gcd (abs 0) by INT_2:34
.= (abs m) gcd 0 by ABSVALUE:2
.= abs m by NEWTON:52 ;
hence  ( 0 gcd m = abs m & 1 gcd m = 1 ) by A1; ::_thesis: verum
end;

theorem Th9: :: WSIERP_1:9
for k being Integer holds 1,k are_relative_prime
proof
let k be Integer; ::_thesis: 1,k are_relative_prime
 1 gcd k = 1 by Th8;
hence  1,k are_relative_prime by INT_2:def_3; ::_thesis: verum
end;

theorem Th10: :: WSIERP_1:10
for a being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l are_relative_prime
proof
let a be Nat; ::_thesis: for k, l being Integer st k,l are_relative_prime holds
k |^ a,l are_relative_prime
let k, l be Integer; ::_thesis: ( k,l are_relative_prime implies k |^ a,l are_relative_prime )
defpred S1[ Nat] means k |^ $1,l are_relative_prime ;
assume A1: k,l are_relative_prime ; ::_thesis: k |^ a,l are_relative_prime
A2: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] )
assume  k |^ a,l are_relative_prime ; ::_thesis: S1[a + 1]
then  k * (k |^ a),l are_relative_prime by A1, INT_2:26;
hence  S1[a + 1] by NEWTON:6; ::_thesis: verum
end;
 k |^ 0 = 1 by NEWTON:4;
then A3: S1[ 0 ] by Th9;
 for a being Nat holds S1[a] from NAT_1:sch_2(A3, A2);
hence  k |^ a,l are_relative_prime ; ::_thesis: verum
end;

theorem Th11: :: WSIERP_1:11
for a, b being Nat
for k, l being Integer st k,l are_relative_prime holds
k |^ a,l |^ b are_relative_prime
proof
let a, b be Nat; ::_thesis: for k, l being Integer st k,l are_relative_prime holds
k |^ a,l |^ b are_relative_prime
let k, l be Integer; ::_thesis: ( k,l are_relative_prime implies k |^ a,l |^ b are_relative_prime )
assume  k,l are_relative_prime ; ::_thesis: k |^ a,l |^ b are_relative_prime
then  k |^ a,l are_relative_prime by Th10;
hence  k |^ a,l |^ b are_relative_prime by Th10; ::_thesis: verum
end;

theorem Th12: :: WSIERP_1:12
for b, a being Nat
for k, l being Integer st k gcd l = 1 holds
( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
proof
let b, a be Nat; ::_thesis: for k, l being Integer st k gcd l = 1 holds
( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
let k, l be Integer; ::_thesis: ( k gcd l = 1 implies ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) )
assume  k gcd l = 1 ; ::_thesis: ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 )
then  k,l are_relative_prime by INT_2:def_3;
then  ( k,l |^ b are_relative_prime & k |^ a,l |^ b are_relative_prime ) by Th10, Th11;
hence  ( k gcd (l |^ b) = 1 & (k |^ a) gcd (l |^ b) = 1 ) by INT_2:def_3; ::_thesis: verum
end;

theorem :: WSIERP_1:13
for m, k being Integer holds
( abs m divides k iff m divides k )
proof
let m, k be Integer; ::_thesis: ( abs m divides k iff m divides k )
A1: now__::_thesis:_(_m_divides_k_implies_abs_m_divides_k_)
assume  m divides k ; ::_thesis: abs m divides k
then consider l being Integer such that
A2: m * l = k by INT_1:def_3;
now__::_thesis:_abs_m_divides_k
percases ( m >= 0 or m < 0 ) ;
suppose m >= 0 ; ::_thesis: abs m divides k
then  (abs m) * l = k by A2, ABSVALUE:def_1;
hence  abs m divides k by INT_1:def_3; ::_thesis: verum
end;
suppose m < 0 ; ::_thesis: abs m divides k
then (abs m) * (- l) = (- m) * (- l) by ABSVALUE:def_1
.= k by A2 ;
hence  abs m divides k by INT_1:def_3; ::_thesis: verum
end;
end;
end;
hence  abs m divides k ; ::_thesis: verum
end;
now__::_thesis:_(_abs_m_divides_k_implies_m_divides_k_)
assume  abs m divides k ; ::_thesis: m divides k
then consider l being Integer such that
A3: (abs m) * l = k by INT_1:def_3;
now__::_thesis:_m_divides_k
percases ( m >= 0 or m < 0 ) ;
suppose m >= 0 ; ::_thesis: m divides k
then  m * l = k by A3, ABSVALUE:def_1;
hence  m divides k by INT_1:def_3; ::_thesis: verum
end;
suppose m < 0 ; ::_thesis: m divides k
then k = (- m) * l by A3, ABSVALUE:def_1
.= m * (- l) ;
hence  m divides k by INT_1:def_3; ::_thesis: verum
end;
end;
end;
hence  m divides k ; ::_thesis: verum
end;
hence  ( abs m divides k iff m divides k ) by A1; ::_thesis: verum
end;

theorem Th14: :: WSIERP_1:14
for a, b, c being Nat st a divides b holds
a |^ c divides b |^ c
proof
let a, b, c be Nat; ::_thesis: ( a divides b implies a |^ c divides b |^ c )
assume  a divides b ; ::_thesis: a |^ c divides b |^ c
then consider d being Nat such that
A1: a * d = b by NAT_D:def_3;
 b |^ c = (a |^ c) * (d |^ c) by A1, NEWTON:7;
hence  a |^ c divides b |^ c by NAT_D:def_3; ::_thesis: verum
end;

theorem Th15: :: WSIERP_1:15
for a being Nat st a divides 1 holds
a = 1
proof
let a be Nat; ::_thesis: ( a divides 1 implies a = 1 )
assume A1: a divides 1 ; ::_thesis: a = 1
then  a divides 1 + 1 by NAT_D:8;
hence  a = 1 by A1, NEWTON:39; ::_thesis: verum
end;

theorem :: WSIERP_1:16
for d, a, b being Nat st d divides a & a gcd b = 1 holds
d gcd b = 1 by Th15, NEWTON:57;

Lm5:  for a, b being Nat st a <> 0 holds
( a divides b iff b / a is Element of NAT )
proof
let a, b be Nat; ::_thesis: ( a <> 0 implies ( a divides b iff b / a is Element of NAT ) )
assume A1: a <> 0 ; ::_thesis: ( a divides b iff b / a is Element of NAT )
A2: now__::_thesis:_(_a_divides_b_implies_b_/_a_is_Element_of_NAT_)
assume  a divides b ; ::_thesis: b / a is Element of NAT
then consider d being Nat such that
A3: b = a * d by NAT_D:def_3;
reconsider d = d as Element of NAT by ORDINAL1:def_12;
 b = a * d by A3;
hence  b / a is Element of NAT by A1, XCMPLX_1:89; ::_thesis: verum
end;
now__::_thesis:_(_b_/_a_is_Element_of_NAT_implies_a_divides_b_)
assume  b / a is Element of NAT ; ::_thesis: a divides b
then reconsider d = b / a as Element of NAT ;
 b = a * d by A1, XCMPLX_1:87;
hence  a divides b by NAT_D:def_3; ::_thesis: verum
end;
hence  ( a divides b iff b / a is Element of NAT ) by A2; ::_thesis: verum
end;

theorem Th17: :: WSIERP_1:17
for k, l being Integer st k <> 0 holds
( k divides l iff l / k is Integer )
proof
let k, l be Integer; ::_thesis: ( k <> 0 implies ( k divides l iff l / k is Integer ) )
assume A1: k <> 0 ; ::_thesis: ( k divides l iff l / k is Integer )
A2: now__::_thesis:_(_l_/_k_is_Integer_implies_k_divides_l_)
assume  l / k is Integer ; ::_thesis: k divides l
then reconsider m = l / k as Integer ;
 l = k * m by A1, XCMPLX_1:87;
hence  k divides l by INT_1:def_3; ::_thesis: verum
end;
now__::_thesis:_(_k_divides_l_implies_l_/_k_is_Integer_)
assume  k divides l ; ::_thesis: l / k is Integer
then  ex m being Integer st l = k * m by INT_1:def_3;
hence  l / k is Integer by A1, XCMPLX_1:89; ::_thesis: verum
end;
hence  ( k divides l iff l / k is Integer ) by A2; ::_thesis: verum
end;

Lm6:  for b, a being Nat
for k being Integer st b <> 0 & a * k = b holds
k is Element of NAT
proof
let b, a be Nat; ::_thesis: for k being Integer st b <> 0 & a * k = b holds
k is Element of NAT
let k be Integer; ::_thesis: ( b <> 0 & a * k = b implies k is Element of NAT )
assume that
A1: b <> 0 and
A2: a * k = b ; ::_thesis: k is Element of NAT
A3: a divides b by A2, INT_1:def_3;
A4: a <> 0 by A1, A2;
then  k = b / a by A2, XCMPLX_1:89;
hence  k is Element of NAT by A3, A4, Lm5; ::_thesis: verum
end;

Lm7:  for a, b, c being Nat st a + b <= c holds
( a <= c & b <= c )
proof
let a, b, c be Nat; ::_thesis: ( a + b <= c implies ( a <= c & b <= c ) )
A1: ( a <= a + b & b <= a + b ) by NAT_1:11;
assume  a + b <= c ; ::_thesis: ( a <= c & b <= c )
hence  ( a <= c & b <= c ) by A1, XXREAL_0:2; ::_thesis: verum
end;

theorem :: WSIERP_1:18
for a, b, c being Nat st a <= b - c holds
( a <= b & c <= b )
proof
let a, b, c be Nat; ::_thesis: ( a <= b - c implies ( a <= b & c <= b ) )
assume  a <= b - c ; ::_thesis: ( a <= b & c <= b )
then  a + c <= b by XREAL_1:19;
hence  ( a <= b & c <= b ) by Lm7; ::_thesis: verum
end;

Lm8:  for k, m being Integer holds
( k < m iff k <= m - 1 )
proof
let k, m be Integer; ::_thesis: ( k < m iff k <= m - 1 )
A1: now__::_thesis:_(_k_<=_m_-_1_implies_k_<_m_)
assume  k <= m - 1 ; ::_thesis: k < m
then A2: k + 1 <= m by XREAL_1:19;
 k < k + 1 by XREAL_1:29;
hence  k < m by A2, XXREAL_0:2; ::_thesis: verum
end;
now__::_thesis:_(_k_<_m_implies_k_<=_m_-_1_)
assume  k < m ; ::_thesis: k <= m - 1
then  k + 1 <= m by INT_1:7;
hence  k <= m - 1 by XREAL_1:19; ::_thesis: verum
end;
hence  ( k < m iff k <= m - 1 ) by A1; ::_thesis: verum
end;

Lm9:  for k, m being Integer holds
( k < m + 1 iff k <= m )
proof
let k, m be Integer; ::_thesis: ( k < m + 1 iff k <= m )
 ( k < m + 1 iff k - 1 < m ) by XREAL_1:19;
hence  ( k < m + 1 iff k <= m ) by Lm8; ::_thesis: verum
end;


definition
let D be non empty set ;
let D1 be non empty Subset of D;
let f1, f2 be FinSequence of D1;
:: original: ^
redefine funcf1 ^ f2 ->  FinSequence of D1;
coherence
 f1 ^ f2 is FinSequence of D1
proof
thus  rng (f1 ^ f2) c= D1 by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
end;


registration
let fr be FinSequence of INT ;
cluster Product fr ->  integer ;
coherence
 Product fr is integer
proof
defpred S1[ FinSequence of INT ] means  Product fr is Integer;
A1: now__::_thesis:_for_s_being_FinSequence_of_INT_
for_m_being_Element_of_INT_st_S1[s]_holds_
S1[s_^_<*m*>]
let s be FinSequence of INT ; ::_thesis: for m being Element of INT st S1[s] holds
S1[s ^ <*m*>]
let m be Element of INT ; ::_thesis: ( S1[s] implies S1[s ^ <*m*>] )
reconsider k = m as Integer ;
assume  S1[s] ; ::_thesis: S1[s ^ <*m*>]
then reconsider pis = Product s as Integer ;
 Product (s ^ <*m*>) = pis * k by RVSUM_1:96;
hence  S1[s ^ <*m*>] ; ::_thesis: verum
end;
A2: S1[ <*> INT] by RVSUM_1:94;
 for fr1 being FinSequence of INT holds S1[fr1] from FINSEQ_2:sch_2(A2, A1);
hence  Product fr is integer ; ::_thesis: verum
end;
end;

definition
let fp be FinSequence of NAT ;
:: original: Sum
redefine func Sum fp ->  Element of NAT ;
coherence
 Sum fp is Element of NAT
proof
defpred S1[ set ] means  ex f being FinSequence of NAT st
( f = $1 & Sum f is Element of NAT );
A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_
for_a_being_Element_of_NAT_st_S1[fp]_holds_
S1[fp_^_<*a*>]
let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds
S1[fp ^ <*a*>]
let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] )
assume  S1[fp] ; ::_thesis: S1[fp ^ <*a*>]
then reconsider sp = Sum fp as Element of NAT ;
 Sum (fp ^ <*a*>) = sp + a by RVSUM_1:74;
hence  S1[fp ^ <*a*>] ; ::_thesis: verum
end;
A2: S1[ <*> NAT] by RVSUM_1:72;
 for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A2, A1);
then  ex f being FinSequence of NAT st
( f = fp & Sum f is Element of NAT ) ;
hence  Sum fp is Element of NAT ; ::_thesis: verum
end;
end;

definition
let fp be FinSequence of NAT ;
:: original: Product
redefine func Product fp ->  Element of NAT ;
coherence
 Product fp is Element of NAT
proof
defpred S1[ set ] means  ex f being FinSequence of NAT st
( f = $1 & Product f is Element of NAT );
A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_
for_a_being_Element_of_NAT_st_S1[fp]_holds_
S1[fp_^_<*a*>]
let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds
S1[fp ^ <*a*>]
let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] )
assume  S1[fp] ; ::_thesis: S1[fp ^ <*a*>]
then reconsider sp = Product fp as Element of NAT ;
 Product (fp ^ <*a*>) = sp * a by RVSUM_1:96;
hence  S1[fp ^ <*a*>] ; ::_thesis: verum
end;
A2: S1[ <*> NAT] by RVSUM_1:94;
 for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A2, A1);
then  ex f being FinSequence of NAT st
( f = fp & Product f is Element of NAT ) ;
hence  Product fp is Element of NAT ; ::_thesis: verum
end;
end;

Lm10:  for a being Nat
for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
proof
let a be Nat; ::_thesis: for fs being FinSequence st a in dom fs holds
ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
let fs be FinSequence; ::_thesis: ( a in dom fs implies ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) )
assume A1: a in dom fs ; ::_thesis: ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a )
then  ( a >= 1 & a <= len fs ) by FINSEQ_3:25;
then reconsider b = (len fs) - a, d = a - 1 as Element of NAT by INT_1:5;
 len fs = a + b ;
then consider fs3, fs2 being FinSequence such that
A2: len fs3 = a and
A3: len fs2 = b and
A4: fs = fs3 ^ fs2 by FINSEQ_2:22;
 a = d + 1 ;
then consider fs1 being FinSequence, v being set  such that
A5: fs3 = fs1 ^ <*v*> by A2, FINSEQ_2:18;
A6: (len fs1) + 1 = d + 1 by A2, A5, FINSEQ_2:16;
 a <> 0 by A1, FINSEQ_3:25;
then  a in dom fs3 by A2, CARD_1:27, FINSEQ_5:6;
then  fs3 . a = fs . a by A4, FINSEQ_1:def_7;
then  fs . a = v by A5, A6, FINSEQ_1:42;
hence  ex fs1, fs2 being FinSequence st
( fs = (fs1 ^ <*(fs . a)*>) ^ fs2 & len fs1 = a - 1 & len fs2 = (len fs) - a ) by A3, A4, A5, A6; ::_thesis: verum
end;

definition
let a be Nat;
let fs be FinSequence;
redefine func Del (fs,a) means :Def1: :: WSIERP_1:def 1
it = fs if  not a in dom fs
otherwise ( (len it) + 1 = len fs & ( for b being Nat holds
( ( b < a implies it . b = fs . b ) & ( b >= a implies it . b = fs . (b + 1) ) ) ) );
compatibility
 for b1 being set holds
( ( not a in dom fs implies ( b1 = Del (fs,a) iff b1 = fs ) ) & ( a in dom fs implies ( b1 = Del (fs,a) iff ( (len b1) + 1 = len fs & ( for b being Nat holds
( ( b < a implies b1 . b = fs . b ) & ( b >= a implies b1 . b = fs . (b + 1) ) ) ) ) ) ) )
proof
let IT be FinSequence; ::_thesis: ( ( not a in dom fs implies ( IT = Del (fs,a) iff IT = fs ) ) & ( a in dom fs implies ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) ) )
thus  ( not a in dom fs implies ( IT = Del (fs,a) iff IT = fs ) ) by FINSEQ_3:104; ::_thesis: ( a in dom fs implies ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) ) )
assume A1: a in dom fs ; ::_thesis: ( IT = Del (fs,a) iff ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) ) )
hereby  ::_thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ) implies IT = Del (fs,a) )
assume A2: IT = Del (fs,a) ; ::_thesis: ( (len IT) + 1 = len fs & ( for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) ) ) )
then A3: ex m being Nat st
( len fs = m + 1 & len IT = m ) by A1, FINSEQ_3:104;
hence  (len IT) + 1 = len fs ; ::_thesis: for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b2 = fs . (b2 + 1) ) )
let b be Nat; ::_thesis: ( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b1 = fs . (b1 + 1) ) )
thus  ( b < a implies IT . b = fs . b ) by A2, FINSEQ_3:110; ::_thesis: ( b >= a implies IT . b1 = fs . (b1 + 1) )
assume A4: b >= a ; ::_thesis: IT . b1 = fs . (b1 + 1)
percases ( b <= len IT or b > len IT ) ;
suppose b <= len IT ; ::_thesis: IT . b1 = fs . (b1 + 1)
hence  IT . b = fs . (b + 1) by A1, A2, A3, A4, FINSEQ_3:111; ::_thesis: verum
end;
supposeA5: b > len IT ; ::_thesis: IT . b1 = fs . (b1 + 1)
then  not b in dom IT by FINSEQ_3:25;
then A6: IT . b = {} by FUNCT_1:def_2;
 b + 1 > (len IT) + 1 by A5, XREAL_1:6;
then  not b + 1 in dom fs by A3, FINSEQ_3:25;
hence  IT . b = fs . (b + 1) by A6, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
assume that
A7: (len IT) + 1 = len fs and
A8: for b being Nat holds
( ( b < a implies IT . b = fs . b ) & ( b >= a implies IT . b = fs . (b + 1) ) ) ; ::_thesis: IT = Del (fs,a)
A9: for k being Nat st 1 <= k & k <= len IT holds
IT . k = (Del (fs,a)) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len IT implies IT . k = (Del (fs,a)) . k )
assume that
 1 <= k and
A10: k <= len IT ; ::_thesis: IT . k = (Del (fs,a)) . k
reconsider k = k as Element of NAT by ORDINAL1:def_12;
percases ( k < a or k >= a ) ;
supposeA11: k < a ; ::_thesis: IT . k = (Del (fs,a)) . k
then  IT . k = fs . k by A8;
hence  IT . k = (Del (fs,a)) . k by A11, FINSEQ_3:110; ::_thesis: verum
end;
supposeA12: k >= a ; ::_thesis: IT . k = (Del (fs,a)) . k
then  IT . k = fs . (k + 1) by A8;
hence  IT . k = (Del (fs,a)) . k by A1, A7, A10, A12, FINSEQ_3:111; ::_thesis: verum
end;
end;
end;
 ex m being Nat st
( len fs = m + 1 & len (Del (fs,a)) = m ) by A1, FINSEQ_3:104;
hence  IT = Del (fs,a) by A7, A9, FINSEQ_1:14; ::_thesis: verum
end;
correctness
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def1 defines Del WSIERP_1:def_1_:_
 for a being Nat
for fs being FinSequence
for b3 being set holds
( ( not a in dom fs implies ( b3 = Del (fs,a) iff b3 = fs ) ) & ( a in dom fs implies ( b3 = Del (fs,a) iff ( (len b3) + 1 = len fs & ( for b being Nat holds
( ( b < a implies b3 . b = fs . b ) & ( b >= a implies b3 . b = fs . (b + 1) ) ) ) ) ) ) );

Lm11:  for a being Nat
for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
proof
let a be Nat; ::_thesis: for fs, fs1, fs2 being FinSequence
for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
let fs, fs1, fs2 be FinSequence; ::_thesis: for v being set st a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 holds
Del (fs,a) = fs1 ^ fs2
let v be set ; ::_thesis: ( a in dom fs & fs = (fs1 ^ <*v*>) ^ fs2 & len fs1 = a - 1 implies Del (fs,a) = fs1 ^ fs2 )
assume that
A1: a in dom fs and
A2: fs = (fs1 ^ <*v*>) ^ fs2 and
A3: len fs1 = a - 1 ; ::_thesis: Del (fs,a) = fs1 ^ fs2
A4: (len (Del (fs,a))) + 1 = len fs by A1, Def1;
len fs = (len (fs1 ^ <*v*>)) + (len fs2) by A2, FINSEQ_1:22
.= ((len fs1) + 1) + (len fs2) by FINSEQ_2:16
.= a + (len fs2) by A3 ;
then  len (Del (fs,a)) = (len fs2) + (len fs1) by A3, A4;
then A5: len (fs1 ^ fs2) = len (Del (fs,a)) by FINSEQ_1:22;
A6: len <*v*> = 1 by FINSEQ_1:39;
A7: fs = fs1 ^ (<*v*> ^ fs2) by A2, FINSEQ_1:32;
then  len fs = (a - 1) + (len (<*v*> ^ fs2)) by A3, FINSEQ_1:22;
then A8: len (<*v*> ^ fs2) = (len fs) - (a - 1) ;
now__::_thesis:_for_e_being_Nat_st_1_<=_e_&_e_<=_len_(Del_(fs,a))_holds_
(fs1_^_fs2)_._e_=_(Del_(fs,a))_._e
let e be Nat; ::_thesis: ( 1 <= e & e <= len (Del (fs,a)) implies (fs1 ^ fs2) . e = (Del (fs,a)) . e )
assume that
A9: 1 <= e and
A10: e <= len (Del (fs,a)) ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
now__::_thesis:_(fs1_^_fs2)_._e_=_(Del_(fs,a))_._e
percases ( e < a or e >= a ) ;
supposeA11: e < a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
then  e <= a - 1 by Lm8;
then A12: e in dom fs1 by A3, A9, FINSEQ_3:25;
hence (fs1 ^ fs2) . e = fs1 . e by FINSEQ_1:def_7
.= fs . e by A7, A12, FINSEQ_1:def_7
.= (Del (fs,a)) . e by A1, A11, Def1 ;
::_thesis: verum
end;
supposeA13: e >= a ; ::_thesis: (fs1 ^ fs2) . e = (Del (fs,a)) . e
then A14: e > a - 1 by Lm8;
then A15: e + 1 > a by XREAL_1:19;
then  (e + 1) - a > 0 by XREAL_1:50;
then A16: ((e + 1) - a) + 1 > 0 + 1 by XREAL_1:6;
A17: e + 1 > a - 1 by A15, XREAL_1:146, XXREAL_0:2;
then  (e + 1) - (a - 1) > 0 by XREAL_1:50;
then reconsider f = (e + 1) - (a - 1) as Element of NAT by INT_1:3;
A18: e + 1 <= len fs by A4, A10, XREAL_1:6;
then A19: (e + 1) - (a - 1) <= len (<*v*> ^ fs2) by A8, XREAL_1:9;
thus (fs1 ^ fs2) . e = fs2 . (e - (len fs1)) by A3, A5, A10, A14, FINSEQ_1:24
.= fs2 . (f - 1) by A3
.= (<*v*> ^ fs2) . f by A6, A16, A19, FINSEQ_1:24
.= (fs1 ^ (<*v*> ^ fs2)) . (e + 1) by A3, A7, A17, A18, FINSEQ_1:24
.= (Del (fs,a)) . e by A1, A7, A13, Def1 ; ::_thesis: verum
end;
end;
end;
hence  (fs1 ^ fs2) . e = (Del (fs,a)) . e ; ::_thesis: verum
end;
hence  Del (fs,a) = fs1 ^ fs2 by A5, FINSEQ_1:14; ::_thesis: verum
end;

Lm12:  for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs
proof
let a be Nat; ::_thesis: for fs being FinSequence holds dom (Del (fs,a)) c= dom fs
let fs be FinSequence; ::_thesis: dom (Del (fs,a)) c= dom fs
now__::_thesis:_(_a_in_dom_fs_implies_dom_(Del_(fs,a))_c=_dom_fs_)
assume A1: a in dom fs ; ::_thesis: dom (Del (fs,a)) c= dom fs
dom fs = Seg (len fs) by FINSEQ_1:def_3
.= Seg ((len (Del (fs,a))) + 1) by A1, Def1
.= (Seg (len (Del (fs,a)))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:9
.= (dom (Del (fs,a))) \/ {((len (Del (fs,a))) + 1)} by FINSEQ_1:def_3 ;
hence  dom (Del (fs,a)) c= dom fs by XBOOLE_1:7; ::_thesis: verum
end;
hence  dom (Del (fs,a)) c= dom fs by Def1; ::_thesis: verum
end;

definition
let D be non empty set ;
let a be Nat;
let fs be FinSequence of D;
:: original: Del
redefine func Del (fs,a) ->  FinSequence of D;
coherence
 Del (fs,a) is FinSequence of D
proof
 ( rng fs c= D & rng (Del (fs,a)) c= rng fs ) by FINSEQ_1:def_4, FINSEQ_3:106;
hence  rng (Del (fs,a)) c= D by XBOOLE_1:1; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
end;

definition
let D be non empty set ;
let D1 be non empty Subset of D;
let a be Nat;
let fs be FinSequence of D1;
:: original: Del
redefine func Del (fs,a) ->  FinSequence of D1;
coherence
 Del (fs,a) is FinSequence of D1
proof
thus  rng (Del (fs,a)) c= D1 by FINSEQ_1:def_4; :: according to FINSEQ_1:def_4 ::_thesis: verum
end;
end;

Lm13:  for a being Nat
for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )
proof
let a be Nat; ::_thesis: for fs1, fs2 being FinSequence holds
( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )
let fs1, fs2 be FinSequence; ::_thesis: ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) )
set f = fs1 ^ fs2;
A1: len (fs1 ^ fs2) = (len fs1) + (len fs2) by FINSEQ_1:22;
A2: now__::_thesis:_(_a_>=_1_implies_Del_((fs1_^_fs2),((len_fs1)_+_a))_=_fs1_^_(Del_(fs2,a))_)
set f2 = fs1 ^ (Del (fs2,a));
set f1 = Del ((fs1 ^ fs2),((len fs1) + a));
assume A3: a >= 1 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a))
now__::_thesis:_Del_((fs1_^_fs2),((len_fs1)_+_a))_=_fs1_^_(Del_(fs2,a))
percases ( a > len fs2 or a <= len fs2 ) ;
supposeA4: a > len fs2 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a))
then A5: not a in dom fs2 by FINSEQ_3:25;
 (len fs1) + a > len (fs1 ^ fs2) by A1, A4, XREAL_1:6;
then  not (len fs1) + a in dom (fs1 ^ fs2) by FINSEQ_3:25;
hence  Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ fs2 by Def1
.= fs1 ^ (Del (fs2,a)) by A5, Def1 ;
::_thesis: verum
end;
supposeA6: a <= len fs2 ; ::_thesis: Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a))
then A7: a in dom fs2 by A3, FINSEQ_3:25;
 a - 1 >= 0 by A3, XREAL_1:48;
then A8: (len fs1) + (a - 1) >= len fs1 by Lm1;
A9: (len fs1) + a >= 1 by A3, NAT_1:12;
 (len fs1) + a <= len (fs1 ^ fs2) by A1, A6, XREAL_1:6;
then A10: (len fs1) + a in dom (fs1 ^ fs2) by A9, FINSEQ_3:25;
then consider g1, g2 being FinSequence such that
A11: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 and
A12: len g1 = ((len fs1) + a) - 1 and
 len g2 = (len (fs1 ^ fs2)) - ((len fs1) + a) by Lm10;
A13: Del ((fs1 ^ fs2),((len fs1) + a)) = g1 ^ g2 by A10, A11, A12, Lm11;
 fs1 ^ fs2 = g1 ^ (<*((fs1 ^ fs2) . ((len fs1) + a))*> ^ g2) by A11, FINSEQ_1:32;
then consider t being FinSequence such that
A14: fs1 ^ t = g1 by A12, A8, FINSEQ_1:47;
fs1 ^ ((t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2) = (fs1 ^ (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>)) ^ g2 by FINSEQ_1:32
.= fs1 ^ fs2 by A11, A14, FINSEQ_1:32 ;
then A15: fs2 = (t ^ <*((fs1 ^ fs2) . ((len fs1) + a))*>) ^ g2 by FINSEQ_1:33;
 (len fs1) + (a - 1) = (len fs1) + (len t) by A12, A14, FINSEQ_1:22;
then  Del (fs2,a) = t ^ g2 by A7, A15, Lm11;
hence  Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) by A13, A14, FINSEQ_1:32; ::_thesis: verum
end;
end;
end;
hence  Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ; ::_thesis: verum
end;
now__::_thesis:_(_a_<=_len_fs1_implies_Del_((fs1_^_fs2),a)_=_(Del_(fs1,a))_^_fs2_)
set f3 = <*((fs1 ^ fs2) . a)*>;
set f2 = (Del (fs1,a)) ^ fs2;
set f1 = Del ((fs1 ^ fs2),a);
assume A16: a <= len fs1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2
 len fs1 <= len (fs1 ^ fs2) by A1, NAT_1:11;
then A17: a <= len (fs1 ^ fs2) by A16, XXREAL_0:2;
now__::_thesis:_Del_((fs1_^_fs2),a)_=_(Del_(fs1,a))_^_fs2
percases ( a < 1 or a >= 1 ) ;
supposeA18: a < 1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2
then A19: not a in dom fs1 by FINSEQ_3:25;
 not a in dom (fs1 ^ fs2) by A18, FINSEQ_3:25;
hence  Del ((fs1 ^ fs2),a) = fs1 ^ fs2 by Def1
.= (Del (fs1,a)) ^ fs2 by A19, Def1 ;
::_thesis: verum
end;
supposeA20: a >= 1 ; ::_thesis: Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2
then A21: a in dom (fs1 ^ fs2) by A17, FINSEQ_3:25;
then consider g1, g2 being FinSequence such that
A22: fs1 ^ fs2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 and
A23: len g1 = a - 1 and
 len g2 = (len (fs1 ^ fs2)) - a by Lm10;
len (g1 ^ <*((fs1 ^ fs2) . a)*>) = (a - 1) + 1 by A23, FINSEQ_2:16
.= a ;
then consider t being FinSequence such that
A24: fs1 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ t by A16, A22, FINSEQ_1:47;
 (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ g2 = (g1 ^ <*((fs1 ^ fs2) . a)*>) ^ (t ^ fs2) by A22, A24, FINSEQ_1:32;
then A25: g2 = t ^ fs2 by FINSEQ_1:33;
 a in dom fs1 by A16, A20, FINSEQ_3:25;
then A26: Del (fs1,a) = g1 ^ t by A23, A24, Lm11;
thus  Del ((fs1 ^ fs2),a) = g1 ^ g2 by A21, A22, A23, Lm11
.= (Del (fs1,a)) ^ fs2 by A26, A25, FINSEQ_1:32 ; ::_thesis: verum
end;
end;
end;
hence  Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ; ::_thesis: verum
end;
hence  ( ( a <= len fs1 implies Del ((fs1 ^ fs2),a) = (Del (fs1,a)) ^ fs2 ) & ( a >= 1 implies Del ((fs1 ^ fs2),((len fs1) + a)) = fs1 ^ (Del (fs2,a)) ) ) by A2; ::_thesis: verum
end;

Lm14:  for fs being FinSequence
for v being set holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
proof
let fs be FinSequence; ::_thesis: for v being set holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
let v be set ; ::_thesis: ( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs )
A1: len <*v*> = 1 by FINSEQ_1:39;
then  1 in dom <*v*> by FINSEQ_3:25;
then  (len (Del (<*v*>,1))) + 1 = 1 by A1, Def1;
then A2: Del (<*v*>,1) = {} ;
 ( 1 <= len <*v*> & {} ^ fs = fs ) by FINSEQ_1:34, FINSEQ_1:39;
hence  Del ((<*v*> ^ fs),1) = fs by A2, Lm13; ::_thesis: Del ((fs ^ <*v*>),((len fs) + 1)) = fs
 fs ^ {} = fs by FINSEQ_1:34;
hence  Del ((fs ^ <*v*>),((len fs) + 1)) = fs by A2, Lm13; ::_thesis: verum
end;

theorem :: WSIERP_1:19
for v1, v2, v3 being set holds
( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
proof
let v1, v2, v3 be set ; ::_thesis: ( Del (<*v1*>,1) = {} & Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus  Del (<*v1*>,1) = Del ((<*v1*> ^ {}),1) by FINSEQ_1:34
.= {} by Lm14 ; ::_thesis: ( Del (<*v1,v2*>,1) = <*v2*> & Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus  Del (<*v1,v2*>,1) = <*v2*> by Lm14; ::_thesis: ( Del (<*v1,v2*>,2) = <*v1*> & Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
 len <*v1*> = 1 by FINSEQ_1:39;
hence A1: Del (<*v1,v2*>,2) = Del ((<*v1*> ^ <*v2*>),((len <*v1*>) + 1))
.= <*v1*> by Lm14 ;
::_thesis: ( Del (<*v1,v2,v3*>,1) = <*v2,v3*> & Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
thus  Del (<*v1,v2,v3*>,1) = Del ((<*v1*> ^ <*v2,v3*>),1) by FINSEQ_1:43
.= <*v2,v3*> by Lm14 ; ::_thesis: ( Del (<*v1,v2,v3*>,2) = <*v1,v3*> & Del (<*v1,v2,v3*>,3) = <*v1,v2*> )
A2: len <*v1,v2*> = 2 by FINSEQ_1:44;
hence  Del (<*v1,v2,v3*>,2) = <*v1,v3*> by A1, Lm13; ::_thesis: Del (<*v1,v2,v3*>,3) = <*v1,v2*>
 (len <*v1,v2*>) + 1 = 3 by A2;
hence  Del (<*v1,v2,v3*>,3) = <*v1,v2*> by Lm14; ::_thesis: verum
end;

Lm15:  for fs being FinSequence st 1 <= len fs holds
( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
proof
let fs be FinSequence; ::_thesis: ( 1 <= len fs implies ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> ) )
set fs1 = <*(fs . 1)*> ^ (Del (fs,1));
set fs2 = (Del (fs,(len fs))) ^ <*(fs . (len fs))*>;
A1: len <*(fs . 1)*> = 1 by FINSEQ_1:39;
assume A2: 1 <= len fs ; ::_thesis: ( fs = <*(fs . 1)*> ^ (Del (fs,1)) & fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> )
then A3: len fs in dom fs by FINSEQ_3:25;
A4: 1 in dom fs by A2, FINSEQ_3:25;
then A5: len fs = (len <*(fs . 1)*>) + (len (Del (fs,1))) by A1, Def1
.= len (<*(fs . 1)*> ^ (Del (fs,1))) by FINSEQ_1:22 ;
 for b being Nat st 1 <= b & b <= len fs holds
fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b
proof
let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b )
assume that
A6: 1 <= b and
A7: b <= len fs ; ::_thesis: fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b
now__::_thesis:_(<*(fs_._1)*>_^_(Del_(fs,1)))_._b_=_fs_._b
percases ( b = 1 or b > 1 ) by A6, XXREAL_0:1;
supposeA8: b = 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b
 1 in dom <*(fs . 1)*> by A1, FINSEQ_3:25;
hence (<*(fs . 1)*> ^ (Del (fs,1))) . b = <*(fs . 1)*> . 1 by A8, FINSEQ_1:def_7
.= fs . b by A8, FINSEQ_1:40 ;
::_thesis: verum
end;
supposeA9: b > 1 ; ::_thesis: (<*(fs . 1)*> ^ (Del (fs,1))) . b = fs . b
then A10: b - 1 > 0 by XREAL_1:50;
then reconsider e = b - 1 as Element of NAT by INT_1:3;
A11: e >= 1 by A10, NAT_1:14;
thus (<*(fs . 1)*> ^ (Del (fs,1))) . b = (Del (fs,1)) . e by A1, A5, A7, A9, FINSEQ_1:24
.= fs . (e + 1) by A4, A11, Def1
.= fs . b ; ::_thesis: verum
end;
end;
end;
hence  fs . b = (<*(fs . 1)*> ^ (Del (fs,1))) . b ; ::_thesis: verum
end;
hence  <*(fs . 1)*> ^ (Del (fs,1)) = fs by A5, FINSEQ_1:14; ::_thesis: fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*>
 len <*(fs . (len fs))*> = 1 by FINSEQ_1:39;
then A12: len fs = (len <*(fs . (len fs))*>) + (len (Del (fs,(len fs)))) by A3, Def1
.= len ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) by FINSEQ_1:22 ;
A13: (len (Del (fs,(len fs)))) + 1 = len fs by A3, Def1;
then A14: len (Del (fs,(len fs))) = (len fs) - 1 ;
 for b being Nat st 1 <= b & b <= len fs holds
fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b
proof
let b be Nat; ::_thesis: ( 1 <= b & b <= len fs implies fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b )
assume that
A15: 1 <= b and
A16: b <= len fs ; ::_thesis: fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b
now__::_thesis:_((Del_(fs,(len_fs)))_^_<*(fs_._(len_fs))*>)_._b_=_fs_._b
percases ( b = len fs or b < len fs ) by A16, XXREAL_0:1;
supposeA17: b = len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b
reconsider e = b - (b - 1) as Element of NAT ;
thus ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = <*(fs . (len fs))*> . e by A13, A12, A17, FINSEQ_1:24, XREAL_1:146
.= fs . b by A17, FINSEQ_1:40 ; ::_thesis: verum
end;
supposeA18: b < len fs ; ::_thesis: ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = fs . b
then  b + 1 <= len fs by NAT_1:13;
then  b <= len (Del (fs,(len fs))) by A14, XREAL_1:19;
then  b in dom (Del (fs,(len fs))) by A15, FINSEQ_3:25;
hence ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b = (Del (fs,(len fs))) . b by FINSEQ_1:def_7
.= fs . b by A3, A18, Def1 ;
::_thesis: verum
end;
end;
end;
hence  fs . b = ((Del (fs,(len fs))) ^ <*(fs . (len fs))*>) . b ; ::_thesis: verum
end;
hence  fs = (Del (fs,(len fs))) ^ <*(fs . (len fs))*> by A12, FINSEQ_1:14; ::_thesis: verum
end;

Lm16:  for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Product (Del (ft,a))) * (ft . a) = Product ft
proof
let a be Nat; ::_thesis: for ft being FinSequence of REAL st a in dom ft holds
(Product (Del (ft,a))) * (ft . a) = Product ft
let ft be FinSequence of REAL ; ::_thesis: ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft )
defpred S1[ Nat] means ( $1 in dom ft implies (ft . $1) * (Product (Del (ft,$1))) = Product ft );
A1: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] )
assume  S1[a] ; ::_thesis: S1[a + 1]
now__::_thesis:_S1[a_+_1]
percases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ;
supposeA2: a = 0 ; ::_thesis: S1[a + 1]
thus  S1[a + 1] ::_thesis: verum
proof
assume  a + 1 in dom ft ; ::_thesis: (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft
then  a + 1 <= len ft by FINSEQ_3:25;
then  <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm15;
then  Product ft = (Product <*(ft . 1)*>) * (Product (Del (ft,1))) by RVSUM_1:97
.= (ft . 1) * (Product (Del (ft,1))) by RVSUM_1:95 ;
hence  (ft . (a + 1)) * (Product (Del (ft,(a + 1)))) = Product ft by A2; ::_thesis: verum
end;
end;
suppose ( a > 0 & a < len ft ) ; ::_thesis: S1[a + 1]
then  ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13;
then A3: a + 1 in dom ft by FINSEQ_3:25;
then consider fs1, fs2 being FinSequence such that
A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and
A5: len fs1 = (a + 1) - 1 and
 len fs2 = (len ft) - (a + 1) by Lm10;
A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm11;
reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36;
reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36;
Product ft = (Product (fs1 ^ <*(ft . (a + 1))*>)) * (Product fs2) by A4, RVSUM_1:97
.= ((Product fs1) * (Product <*(ft . (a + 1))*>)) * (Product fs2) by RVSUM_1:97
.= ((ft . (a + 1)) * (Product fs1)) * (Product fs2) by RVSUM_1:95
.= (ft . (a + 1)) * ((Product fs1) * (Product fs2)) ;
hence  S1[a + 1] by A6, RVSUM_1:97; ::_thesis: verum
end;
suppose a >= len ft ; ::_thesis: S1[a + 1]
then  len ft < a + 1 by NAT_1:13;
hence  S1[a + 1] by FINSEQ_3:25; ::_thesis: verum
end;
end;
end;
hence  S1[a + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ] by FINSEQ_3:25;
 for a being Nat holds S1[a] from NAT_1:sch_2(A7, A1);
hence  ( a in dom ft implies (Product (Del (ft,a))) * (ft . a) = Product ft ) ; ::_thesis: verum
end;

theorem :: WSIERP_1:20
for a being Nat
for ft being FinSequence of REAL st a in dom ft holds
(Sum (Del (ft,a))) + (ft . a) = Sum ft
proof
let a be Nat; ::_thesis: for ft being FinSequence of REAL st a in dom ft holds
(Sum (Del (ft,a))) + (ft . a) = Sum ft
let ft be FinSequence of REAL ; ::_thesis: ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft )
defpred S1[ Nat] means ( $1 in dom ft implies (ft . $1) + (Sum (Del (ft,$1))) = Sum ft );
A1: for a being Nat st S1[a] holds
S1[a + 1]
proof
let a be Nat; ::_thesis: ( S1[a] implies S1[a + 1] )
assume  S1[a] ; ::_thesis: S1[a + 1]
now__::_thesis:_S1[a_+_1]
percases ( a = 0 or ( a > 0 & a < len ft ) or a >= len ft ) ;
supposeA2: a = 0 ; ::_thesis: S1[a + 1]
thus  S1[a + 1] ::_thesis: verum
proof
assume  a + 1 in dom ft ; ::_thesis: (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft
then  a + 1 <= len ft by FINSEQ_3:25;
then  <*(ft . 1)*> ^ (Del (ft,1)) = ft by A2, Lm15;
then  Sum ft = (Sum <*(ft . 1)*>) + (Sum (Del (ft,1))) by RVSUM_1:75
.= (ft . 1) + (Sum (Del (ft,1))) by FINSOP_1:11 ;
hence  (ft . (a + 1)) + (Sum (Del (ft,(a + 1)))) = Sum ft by A2; ::_thesis: verum
end;
end;
suppose ( a > 0 & a < len ft ) ; ::_thesis: S1[a + 1]
then  ( a + 1 >= 1 & a + 1 <= len ft ) by NAT_1:11, NAT_1:13;
then A3: a + 1 in dom ft by FINSEQ_3:25;
then consider fs1, fs2 being FinSequence such that
A4: ft = (fs1 ^ <*(ft . (a + 1))*>) ^ fs2 and
A5: len fs1 = (a + 1) - 1 and
 len fs2 = (len ft) - (a + 1) by Lm10;
A6: Del (ft,(a + 1)) = fs1 ^ fs2 by A3, A4, A5, Lm11;
reconsider fs2 = fs2 as FinSequence of REAL by A4, FINSEQ_1:36;
reconsider fs1 = fs1 as FinSequence of REAL by A6, FINSEQ_1:36;
Sum ft = (Sum (fs1 ^ <*(ft . (a + 1))*>)) + (Sum fs2) by A4, RVSUM_1:75
.= ((Sum fs1) + (Sum <*(ft . (a + 1))*>)) + (Sum fs2) by RVSUM_1:75
.= ((ft . (a + 1)) + (Sum fs1)) + (Sum fs2) by FINSOP_1:11
.= (ft . (a + 1)) + ((Sum fs1) + (Sum fs2)) ;
hence  S1[a + 1] by A6, RVSUM_1:75; ::_thesis: verum
end;
suppose a >= len ft ; ::_thesis: S1[a + 1]
then  a + 1 > len ft by NAT_1:13;
hence  S1[a + 1] by FINSEQ_3:25; ::_thesis: verum
end;
end;
end;
hence  S1[a + 1] ; ::_thesis: verum
end;
A7: S1[ 0 ] by FINSEQ_3:25;
 for a being Nat holds S1[a] from NAT_1:sch_2(A7, A1);
hence  ( a in dom ft implies (Sum (Del (ft,a))) + (ft . a) = Sum ft ) ; ::_thesis: verum
end;

theorem :: WSIERP_1:21
for a being Nat
for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Element of NAT
proof
let a be Nat; ::_thesis: for fp being FinSequence of NAT st a in dom fp holds
(Product fp) / (fp . a) is Element of NAT
let fp be FinSequence of NAT ; ::_thesis: ( a in dom fp implies (Product fp) / (fp . a) is Element of NAT )
assume  a in dom fp ; ::_thesis: (Product fp) / (fp . a) is Element of NAT
then consider fs1, fs2 being FinSequence such that
A1: fp = (fs1 ^ <*(fp . a)*>) ^ fs2 and
 len fs1 = a - 1 and
 len fs2 = (len fp) - a by Lm10;
percases ( fp . a <> 0 or fp . a = 0 ) ;
supposeA2: fp . a <> 0 ; ::_thesis: (Product fp) / (fp . a) is Element of NAT
reconsider fs2 = fs2 as FinSequence of NAT by A1, FINSEQ_1:36;
 fs1 ^ <*(fp . a)*> is FinSequence of NAT by A1, FINSEQ_1:36;
then reconsider fs1 = fs1 as FinSequence of NAT by FINSEQ_1:36;
Product fp = (Product (fs1 ^ <*(fp . a)*>)) * (Product fs2) by A1, RVSUM_1:97
.= ((fp . a) * (Product fs1)) * (Product fs2) by RVSUM_1:96
.= (fp . a) * ((Product fs1) * (Product fs2)) ;
hence  (Product fp) / (fp . a) is Element of NAT by A2, XCMPLX_1:89; ::_thesis: verum
end;
supposeA3: fp . a = 0 ; ::_thesis: (Product fp) / (fp . a) is Element of NAT
(Product fp) / (fp . a) = (Product fp) * ((fp . a) ") by XCMPLX_0:def_9
.= (Product fp) * 0 by A3
.= 0 ;
hence  (Product fp) / (fp . a) is Element of NAT ; ::_thesis: verum
end;
end;
end;

theorem Th22: :: WSIERP_1:22
for q being Rational holds numerator q, denominator q are_relative_prime
proof
let q be Rational; ::_thesis: numerator q, denominator q are_relative_prime
set k = numerator q;
set h = denominator q;
reconsider a = (numerator q) gcd (denominator q) as Element of NAT by INT_2:20;
 a divides numerator q by INT_2:21;
then A1: ex l being Integer st numerator q = a * l by INT_1:def_3;
 (numerator q) gcd (denominator q) divides denominator q by INT_2:21;
then consider b being Nat such that
A2: denominator q = a * b by NAT_D:def_3;
 denominator q <> 0 by RAT_1:def_3;
then  a <> 0 by INT_2:5;
then A3: a >= 0 + 1 by NAT_1:13;
reconsider b = b as Element of NAT by ORDINAL1:def_12;
A4: denominator q = a * b by A2;
assume  not numerator q, denominator q are_relative_prime ; ::_thesis: contradiction
then  a <> 1 by INT_2:def_3;
then  a > 1 by A3, XXREAL_0:1;
hence  contradiction by A1, A4, RAT_1:29; ::_thesis: verum
end;

theorem :: WSIERP_1:23
for a being Nat
for k being Integer
for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
proof
let a be Nat; ::_thesis: for k being Integer
for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
let k be Integer; ::_thesis: for q being Rational st q = k / a & a <> 0 & k,a are_relative_prime holds
( k = numerator q & a = denominator q )
let q be Rational; ::_thesis: ( q = k / a & a <> 0 & k,a are_relative_prime implies ( k = numerator q & a = denominator q ) )
assume that
A1: ( q = k / a & a <> 0 ) and
A2: k,a are_relative_prime ; ::_thesis: ( k = numerator q & a = denominator q )
 a in NAT by ORDINAL1:def_12;
then consider b being Element of NAT  such that
A3: ( k = (numerator q) * b & a = (denominator q) * b ) by A1, RAT_1:27;
 numerator q, denominator q are_relative_prime by Th22;
then  k gcd a = abs b by A3, INT_2:24;
then 1 = abs b by A2, INT_2:def_3
.= b by ABSVALUE:def_1 ;
hence  ( k = numerator q & a = denominator q ) by A3; ::_thesis: verum
end;

theorem Th24: :: WSIERP_1:24
for a, b being Nat st ex q being Rational st a = q |^ b holds
ex k being Integer st a = k |^ b
proof
let a, b be Nat; ::_thesis: ( ex q being Rational st a = q |^ b implies ex k being Integer st a = k |^ b )
given q being Rational such that A1: a = q |^ b ; ::_thesis: ex k being Integer st a = k |^ b
now__::_thesis:_ex_k_being_Integer_st_a_=_k_|^_b
A2: now__::_thesis:_(_b_<>_0_implies_ex_k_being_Integer_st_a_=_k_|^_b_)
set d = denominator q;
set k = numerator q;
assume  b <> 0 ; ::_thesis: ex k being Integer st a = k |^ b
then consider e being Nat such that
A3: e + 1 = b by NAT_1:6;
 denominator q <> 0 by RAT_1:def_3;
then A4: (denominator q) |^ b <> 0 by CARD_4:3;
 (numerator q) |^ b, denominator q are_relative_prime by Th10, Th22;
then A5: ((numerator q) |^ b) gcd (denominator q) = 1 by INT_2:def_3;
A6: q = (numerator q) / (denominator q) by RAT_1:15;
then  a = ((numerator q) |^ b) / ((denominator q) |^ b) by A1, PREPOWER:8;
then  a * ((denominator q) |^ b) = (numerator q) |^ b by A4, XCMPLX_1:87;
then (numerator q) |^ b = a * (((denominator q) |^ e) * (denominator q)) by A3, NEWTON:6
.= (a * ((denominator q) |^ e)) * (denominator q) ;
then  denominator q divides (numerator q) |^ b by INT_1:def_3;
then  ( denominator q = 1 or denominator q = - 1 ) by A5, INT_2:13, INT_2:22;
hence  ex k being Integer st a = k |^ b by A1, A6, INT_2:7; ::_thesis: verum
end;
now__::_thesis:_(_b_=_0_implies_ex_k_being_Integer_st_a_=_k_|^_b_)
assume A7: b = 0 ; ::_thesis: ex k being Integer st a = k |^ b
then  a = 1 by A1, NEWTON:4;
then  a = 1 |^ 0 by NEWTON:4;
hence  ex k being Integer st a = k |^ b by A7; ::_thesis: verum
end;
hence  ex k being Integer st a = k |^ b by A2; ::_thesis: verum
end;
hence  ex k being Integer st a = k |^ b ; ::_thesis: verum
end;

theorem Th25: :: WSIERP_1:25
for a, d being Nat st ex q being Rational st a = q |^ d holds
ex b being Nat st a = b |^ d
proof
let a, d be Nat; ::_thesis: ( ex q being Rational st a = q |^ d implies ex b being Nat st a = b |^ d )
assume  ex q being Rational st a = q |^ d ; ::_thesis: ex b being Nat st a = b |^ d
then consider k being Integer such that
A1: a = k |^ d by Th24;
A2: now__::_thesis:_(_a_=_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
assume A3: a = 0 ; ::_thesis: ex b being Nat st a = b |^ d
then  d <> 0 by A1, NEWTON:4;
then  a = 0 |^ d by A3, NAT_1:14, NEWTON:11;
hence  ex b being Nat st a = b |^ d ; ::_thesis: verum
end;
A4: now__::_thesis:_(_d_<>_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
assume  d <> 0 ; ::_thesis: ex b being Nat st a = b |^ d
now__::_thesis:_(_k_is_not_Element_of_NAT_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
consider e being Nat such that
A5: ( d = 2 * e or d = (2 * e) + 1 ) by Lm4;
consider c being Element of NAT  such that
A6: ( k = c or k = - c ) by INT_1:2;
assume A7: k is not Element of NAT ; ::_thesis: ex b being Nat st a = b |^ d
A8: now__::_thesis:_(_d_=_(2_*_e)_+_1_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
assume  d = (2 * e) + 1 ; ::_thesis: ex b being Nat st a = b |^ d
then  - (c |^ d) = a by A1, A7, A6, Th2;
hence  ex b being Nat st a = b |^ d by A2; ::_thesis: verum
end;
now__::_thesis:_(_d_=_2_*_e_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
assume  d = 2 * e ; ::_thesis: ex b being Nat st a = b |^ d
then  a = c |^ d by A1, A6, Th2;
hence  ex b being Nat st a = b |^ d ; ::_thesis: verum
end;
hence  ex b being Nat st a = b |^ d by A5, A8; ::_thesis: verum
end;
hence  ex b being Nat st a = b |^ d by A1; ::_thesis: verum
end;
now__::_thesis:_(_d_=_0_implies_ex_b_being_Nat_st_a_=_b_|^_d_)
assume A9: d = 0 ; ::_thesis: ex b being Nat st a = b |^ d
then  a = 1 by A1, NEWTON:4;
then  a = 1 |^ 0 by NEWTON:4;
hence  ex b being Nat st a = b |^ d by A9; ::_thesis: verum
end;
hence  ex b being Nat st a = b |^ d by A4; ::_thesis: verum
end;

theorem :: WSIERP_1:26
for e, a, b being Nat st e > 0 & a |^ e divides b |^ e holds
a divides b
proof
let e, a, b be Nat; ::_thesis: ( e > 0 & a |^ e divides b |^ e implies a divides b )
assume that
A1: e > 0 and
A2: a |^ e divides b |^ e ; ::_thesis: a divides b
consider f being Nat such that
A3: (a |^ e) * f = b |^ e by A2, NAT_D:def_3;
A4: a in REAL by XREAL_0:def_1;
A5: now__::_thesis:_(_a_<>_0_&_b_<>_0_implies_a_divides_b_)
assume that
A6: a <> 0 and
 b <> 0 ; ::_thesis: a divides b
 a |^ e <> 0 by A4, A6, CARD_4:3;
then f = (b |^ e) / (a |^ e) by A3, XCMPLX_1:89
.= (b / a) |^ e by PREPOWER:8 ;
then consider d being Nat such that
A7: f = d |^ e by Th25;
 b |^ e = (a * d) |^ e by A3, A7, NEWTON:7;
then  b = a * d by A1, Th3;
hence  a divides b by NAT_D:def_3; ::_thesis: verum
end;
A8: b in REAL by XREAL_0:def_1;
A9: now__::_thesis:_(_a_=_0_implies_a_divides_b_)
assume A10: a = 0 ; ::_thesis: a divides b
then  0 divides b |^ e by A1, A2, NAT_1:14, NEWTON:11;
then  ex f being Nat st 0 * f = b |^ e by NAT_D:def_3;
hence  a divides b by A8, A10, CARD_4:3; ::_thesis: verum
end;
now__::_thesis:_(_b_=_0_implies_a_divides_b_)
assume  b = 0 ; ::_thesis: a divides b
then  a * 0 = b ;
hence  a divides b by NAT_D:def_3; ::_thesis: verum
end;
hence  a divides b by A9, A5; ::_thesis: verum
end;

theorem Th27: :: WSIERP_1:27
for a, b being Nat ex m, n being Integer st a gcd b = (a * m) + (b * n)
proof
let a, b be Nat; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)
A1: for c being Nat ex m, n being Integer st 0 gcd c = (0 * m) + (c * n)
proof
let c be Nat; ::_thesis: ex m, n being Integer st 0 gcd c = (0 * m) + (c * n)
take  0 ; ::_thesis: ex n being Integer st 0 gcd c = (0 * 0) + (c * n)
take  1 ; ::_thesis: 0 gcd c = (0 * 0) + (c * 1)
thus  0 gcd c = (0 * 0) + (c * 1) by NEWTON:52; ::_thesis: verum
end;
now__::_thesis:_ex_m,_n_being_Integer_st_a_gcd_b_=_(a_*_m)_+_(b_*_n)
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
suppose a = 0 ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)
hence  ex m, n being Integer st a gcd b = (a * m) + (b * n) by A1; ::_thesis: verum
end;
supposeA2: b = 0 ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)
then  ex m, n being Integer st a gcd b = (0 * m) + (a * n) by A1;
hence  ex m, n being Integer st a gcd b = (a * m) + (b * n) by A2; ::_thesis: verum
end;
supposeA3: ( a <> 0 & b <> 0 ) ; ::_thesis: ex m, n being Integer st a gcd b = (a * m) + (b * n)
defpred S1[ set ] means  ex m, n being Integer st
( $1 = (a * m) + (b * n) & $1 <> 0 );
 a + b = (a * 1) + (b * 1) ;
then A4: ex c being Nat st S1[c] by A3;
consider d being Nat such that
A5: ( S1[d] & ( for c being Nat st S1[c] holds
d <= c ) ) from NAT_1:sch_5(A4);
consider e, f being Nat such that
A6: a = (d * e) + f and
A7: f < d by A5, NAT_1:17;
consider m, n being Integer such that
A8: d = (a * m) + (b * n) by A5;
A9: now__::_thesis:_not_f_<>_0
assume A10: f <> 0 ; ::_thesis: contradiction
f = a - (d * e) by A6
.= (a * (1 - (m * e))) + (b * (- (n * e))) by A8 ;
hence  contradiction by A5, A7, A10; ::_thesis: verum
end;
consider e, f being Nat such that
A11: b = (d * e) + f and
A12: f < d by A5, NAT_1:17;
now__::_thesis:_not_f_<>_0
assume A13: f <> 0 ; ::_thesis: contradiction
f = b - (d * e) by A11
.= (b * (1 - (n * e))) + (a * (- (m * e))) by A8 ;
hence  contradiction by A5, A12, A13; ::_thesis: verum
end;
then A14: d divides b by A11, NAT_D:def_3;
 d divides a by A6, A9, NAT_D:def_3;
then A15: d divides a gcd b by A14, NAT_D:def_5;
 ( a gcd b divides a & a gcd b divides b ) by NAT_D:def_5;
then  a gcd b divides d by A8, Th5;
hence  ex m, n being Integer st a gcd b = (a * m) + (b * n) by A8, A15, NAT_D:5; ::_thesis: verum
end;
end;
end;
hence  ex m, n being Integer st a gcd b = (a * m) + (b * n) ; ::_thesis: verum
end;

theorem Th28: :: WSIERP_1:28
for m, n being Integer ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
proof
let m, n be Integer; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
 m gcd n = (abs m) gcd (abs n) by INT_2:34;
then consider m1, n1 being Integer such that
A1: ((abs m) * m1) + ((abs n) * n1) = m gcd n by Th27;
now__::_thesis:_ex_m1,_n1_being_Integer_st_m_gcd_n_=_(m_*_m1)_+_(n_*_n1)
percases ( ( m >= 0 & n >= 0 ) or ( m >= 0 & n < 0 ) or ( m < 0 & n >= 0 ) or ( m < 0 & n < 0 ) ) ;
suppose ( m >= 0 & n >= 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
then  ( abs m = m & abs n = n ) by ABSVALUE:def_1;
hence  ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) by A1; ::_thesis: verum
end;
supposeA2: ( m >= 0 & n < 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
then  abs n = - n by ABSVALUE:def_1;
then  m gcd n = (m * m1) + (n * (- n1)) by A1, A2, ABSVALUE:def_1;
hence  ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum
end;
supposeA3: ( m < 0 & n >= 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
then  abs m = - m by ABSVALUE:def_1;
then  m gcd n = (m * (- m1)) + (n * n1) by A1, A3, ABSVALUE:def_1;
hence  ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum
end;
suppose ( m < 0 & n < 0 ) ; ::_thesis: ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1)
then  ( abs m = - m & abs n = - n ) by ABSVALUE:def_1;
then  m gcd n = (m * (- m1)) + (n * (- n1)) by A1;
hence  ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum
end;
end;
end;
hence  ex m1, n1 being Integer st m gcd n = (m * m1) + (n * n1) ; ::_thesis: verum
end;

theorem Th29: :: WSIERP_1:29
for m, n, k being Integer st m divides n * k & m gcd n = 1 holds
m divides k
proof
let m, n, k be Integer; ::_thesis: ( m divides n * k & m gcd n = 1 implies m divides k )
assume that
A1: m divides n * k and
A2: m gcd n = 1 ; ::_thesis: m divides k
consider m1, n1 being Integer such that
A3: (m * m1) + (n * n1) = 1 by A2, Th28;
k = ((m * m1) + (n * n1)) * k by A3
.= (m * (m1 * k)) + ((n * k) * n1) ;
hence  m divides k by A1, Th5; ::_thesis: verum
end;

theorem :: WSIERP_1:30
for a, b, c being Nat st a gcd b = 1 & a divides b * c holds
a divides c by Th29;

theorem Th31: :: WSIERP_1:31
for a, b being Nat st a <> 0 & b <> 0 holds
ex c, d being Nat st a gcd b = (a * c) - (b * d)
proof
let a, b be Nat; ::_thesis: ( a <> 0 & b <> 0 implies ex c, d being Nat st a gcd b = (a * c) - (b * d) )
assume that
A1: a <> 0 and
A2: b <> 0 ; ::_thesis: ex c, d being Nat st a gcd b = (a * c) - (b * d)
consider m, n being Integer such that
A3: a gcd b = (a * m) + (b * n) by Th27;
set k = [/(max ((- (m / b)),(n / a)))\] + 1;
 [/(max ((- (m / b)),(n / a)))\] + 1 > n / a by INT_1:32, XXREAL_0:31;
then  ([/(max ((- (m / b)),(n / a)))\] + 1) * a > n by A1, XREAL_1:77;
then A4: (([/(max ((- (m / b)),(n / a)))\] + 1) * a) - n > 0 by XREAL_1:50;
 [/(max ((- (m / b)),(n / a)))\] + 1 > - (m / b) by INT_1:32, XXREAL_0:31;
then  [/(max ((- (m / b)),(n / a)))\] + 1 > (- m) / b by XCMPLX_1:187;
then  ([/(max ((- (m / b)),(n / a)))\] + 1) * b > - m by A2, XREAL_1:77;
then  (([/(max ((- (m / b)),(n / a)))\] + 1) * b) - (- m) > 0 by XREAL_1:50;
then reconsider e = (([/(max ((- (m / b)),(n / a)))\] + 1) * b) + m, d = (([/(max ((- (m / b)),(n / a)))\] + 1) * a) - n as Element of NAT by A4, INT_1:3;
 (a * e) - (b * d) = ((a * m) + 0) + (b * n) ;
hence  ex c, d being Nat st a gcd b = (a * c) - (b * d) by A3; ::_thesis: verum
end;

theorem :: WSIERP_1:32
for f, g, a, b being Nat st f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g holds
ex e being Nat st
( a = e |^ g & b = e |^ f )
proof
let f, g, a, b be Nat; ::_thesis: ( f > 0 & g > 0 & f gcd g = 1 & a |^ f = b |^ g implies ex e being Nat st
( a = e |^ g & b = e |^ f ) )
assume that
A1: f > 0 and
A2: g > 0 and
A3: f gcd g = 1 and
A4: a |^ f = b |^ g ; ::_thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
A5: b in REAL by XREAL_0:def_1;
A6: a in REAL by XREAL_0:def_1;
now__::_thesis:_ex_e_being_Nat_st_
(_a_=_e_|^_g_&_b_=_e_|^_f_)
percases ( a = 0 or b = 0 or ( a <> 0 & b <> 0 ) ) ;
supposeA7: a = 0 ; ::_thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
then  a |^ f = 0 by A1, NAT_1:14, NEWTON:11;
then A8: b = 0 |^ f by A4, A5, A7, CARD_4:3;
 a = 0 |^ g by A2, A7, CARD_4:3;
hence  ex e being Nat st
( a = e |^ g & b = e |^ f ) by A8; ::_thesis: verum
end;
supposeA9: b = 0 ; ::_thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
then  b |^ g = 0 by A2, NAT_1:14, NEWTON:11;
then A10: a = 0 |^ g by A4, A6, A9, CARD_4:3;
 b = 0 |^ f by A1, A9, CARD_4:3;
hence  ex e being Nat st
( a = e |^ g & b = e |^ f ) by A10; ::_thesis: verum
end;
supposeA11: ( a <> 0 & b <> 0 ) ; ::_thesis: ex e being Nat st
( a = e |^ g & b = e |^ f )
consider c, d being Nat such that
A12: (f * c) - (g * d) = 1 by A1, A2, A3, Th31;
reconsider q = (b |^ c) / (a |^ d) as Rational ;
a = a #Z 1 by PREPOWER:35
.= (a |^ (f * c)) / (a |^ (d * g)) by A11, A12, PREPOWER:43
.= ((a |^ f) |^ c) / (a |^ (d * g)) by NEWTON:9
.= ((b |^ g) |^ c) / ((a |^ d) |^ g) by A4, NEWTON:9
.= (b |^ (g * c)) / ((a |^ d) |^ g) by NEWTON:9
.= ((b |^ c) |^ g) / ((a |^ d) |^ g) by NEWTON:9
.= q |^ g by PREPOWER:8 ;
then consider h being Nat such that
A13: a = h |^ g by Th25;
b |^ g = h |^ (f * g) by A4, A13, NEWTON:9
.= (h |^ f) |^ g by NEWTON:9 ;
then  b = h |^ f by A2, Th3;
hence  ex e being Nat st
( a = e |^ g & b = e |^ f ) by A13; ::_thesis: verum
end;
end;
end;
hence  ex e being Nat st
( a = e |^ g & b = e |^ f ) ; ::_thesis: verum
end;


theorem Th33: :: WSIERP_1:33
for m, n, k being Integer holds
( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )
proof
let m, n, k be Integer; ::_thesis: ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k )
A1: now__::_thesis:_(_m_gcd_n_divides_k_implies_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k_)
assume A2: m gcd n divides k ; ::_thesis: ex x, y being Integer st (m * x) + (n * y) = k
now__::_thesis:_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k
consider m1, n1 being Integer such that
A3: m gcd n = (m * m1) + (n * n1) by Th28;
consider l being Integer such that
A4: (m gcd n) * l = k by A2, INT_1:def_3;
 k = (m * (m1 * l)) + (n * (n1 * l)) by A4, A3;
hence  ex x, y being Integer st (m * x) + (n * y) = k ; ::_thesis: verum
end;
hence  ex x, y being Integer st (m * x) + (n * y) = k ; ::_thesis: verum
end;
now__::_thesis:_(_ex_x,_y_being_Integer_st_(m_*_x)_+_(n_*_y)_=_k_implies_m_gcd_n_divides_k_)
given x, y being Integer such that A5: (m * x) + (n * y) = k ; ::_thesis: m gcd n divides k
 ( m gcd n divides m & m gcd n divides n ) by INT_2:21;
hence  m gcd n divides k by A5, Th5; ::_thesis: verum
end;
hence  ( ex x, y being Integer st (m * x) + (n * y) = k iff m gcd n divides k ) by A1; ::_thesis: verum
end;

theorem :: WSIERP_1:34
for m, n, m1, n1, k being Integer st m <> 0 & n <> 0 & (m * m1) + (n * n1) = k holds
for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )
proof
let m, n, m1, n1, k be Integer; ::_thesis: ( m <> 0 & n <> 0 & (m * m1) + (n * n1) = k implies for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) )
assume that
A1: m <> 0 and
A2: n <> 0 and
A3: (m * m1) + (n * n1) = k ; ::_thesis: for x, y being Integer st (m * x) + (n * y) = k holds
ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )
consider m2, n2 being Integer such that
A4: m = (m gcd n) * m2 and
A5: n = (m gcd n) * n2 and
A6: m2,n2 are_relative_prime by A1, INT_2:23;
A7: m gcd n <> 0 by A1, INT_2:5;
then A8: m2 = m / (m gcd n) by A4, XCMPLX_1:89;
A9: n2 = n / (m gcd n) by A7, A5, XCMPLX_1:89;
A10: n2 gcd m2 = 1 by A6, INT_2:def_3;
let x, y be Integer; ::_thesis: ( (m * x) + (n * y) = k implies ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) )
assume  (m * x) + (n * y) = k ; ::_thesis: ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) )
then  m * (x - m1) = n * (n1 - y) by A3;
then A11: m2 * (x - m1) = (n * (n1 - y)) / (m gcd n) by A8, XCMPLX_1:74
.= n2 * (n1 - y) by A9, XCMPLX_1:74 ;
then  n2 divides m2 * (x - m1) by INT_1:def_3;
then  n2 divides x - m1 by A10, Th29;
then consider t being Integer such that
A12: n2 * t = x - m1 by INT_1:def_3;
A13: n2 <> 0 by A2, A5;
then A14: t = (x - m1) / n2 by A12, XCMPLX_1:89;
A15: m2 <> 0 by A1, A4;
then  (x - m1) / n2 = (n1 - y) / m2 by A13, A11, XCMPLX_1:94;
then  t * m2 = n1 - y by A15, A14, XCMPLX_1:87;
then A16: y = n1 - (t * m2) ;
 x = m1 + (t * n2) by A12;
hence  ex t being Integer st
( x = m1 + (t * (n / (m gcd n))) & y = n1 - (t * (m / (m gcd n))) ) by A8, A9, A16; ::_thesis: verum
end;

theorem :: WSIERP_1:35
for a, b, c, d being Nat st a gcd b = 1 & a * b = c |^ d holds
ex e, f being Nat st
( a = e |^ d & b = f |^ d )
proof
let a, b, c, d be Nat; ::_thesis: ( a gcd b = 1 & a * b = c |^ d implies ex e, f being Nat st
( a = e |^ d & b = f |^ d ) )
assume that
A1: a gcd b = 1 and
A2: a * b = c |^ d ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
set e = a gcd c;
 a gcd c divides c by NAT_D:def_5;
then A3: (a gcd c) |^ d divides c |^ d by Th14;
 a gcd c divides a by NAT_D:def_5;
then  (a gcd c) gcd b = 1 by A1, Th15, NEWTON:57;
then  ((a gcd c) |^ d) gcd b = 1 by Th12;
then  (a gcd c) |^ d divides a by A2, A3, Th29;
then consider g being Nat such that
A4: ((a gcd c) |^ d) * g = a by NAT_D:def_3;
reconsider g = g as Element of NAT by ORDINAL1:def_12;
A5: now__::_thesis:_(_d_<>_0_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
A6: c in REAL by XREAL_0:def_1;
assume A7: d <> 0 ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then consider d1 being Nat such that
A8: d = 1 + d1 by NAT_1:10, NAT_1:14;
reconsider d1 = d1 as Element of NAT by ORDINAL1:def_12;
A9: d >= 1 by A7, NAT_1:14;
A10: now__::_thesis:_(_a_gcd_c_<>_0_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
assume A11: a gcd c <> 0 ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A12: ( a <> 0 or c <> 0 ) by INT_2:5;
then A13: a <> 0 by A2, A6, CARD_4:3;
A14: now__::_thesis:_(_c_<>_0_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
reconsider e1 = a gcd c as Real by XREAL_0:def_1;
assume A15: c <> 0 ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then consider a1, c1 being Integer such that
A16: a = (a gcd c) * a1 and
A17: (a gcd c) * c1 = c and
A18: a1,c1 are_relative_prime by INT_2:23;
reconsider a1 = a1, c1 = c1 as Element of NAT by A13, A15, A16, A17, Lm6;
a1 = (((a gcd c) |^ (d1 + 1)) * g) / (a gcd c) by A4, A8, A11, A16, XCMPLX_1:89
.= (((a gcd c) * ((a gcd c) |^ d1)) * g) / (a gcd c) by NEWTON:6
.= ((a gcd c) * (((a gcd c) |^ d1) * g)) / (a gcd c)
.= ((a gcd c) |^ d1) * g by A11, XCMPLX_1:89 ;
then A19: g divides a1 by NAT_D:def_3;
 a1 gcd c1 = 1 by A18, INT_2:def_3;
then  g gcd c1 = 1 by A19, Th15, NEWTON:57;
then A20: g gcd (c1 |^ d) = 1 by Th12;
A21: e1 |^ d <> 0 by A11, CARD_4:3;
 c1 = c / (a gcd c) by A11, A17, XCMPLX_1:89;
then A22: c1 |^ d = (((a gcd c) |^ d) * (g * b)) / ((a gcd c) |^ d) by A2, A4, PREPOWER:8
.= g * b by A21, XCMPLX_1:89 ;
then  g divides c1 |^ d by NAT_D:def_3;
then  g = 1 by A20, NEWTON:49;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A4, A22; ::_thesis: verum
end;
now__::_thesis:_(_0_=_c_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
assume  0 = c ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A23: b = 0 by A2, A9, A12, NEWTON:11, XCMPLX_1:6;
then  a = 1 by A1, NEWTON:52;
then A24: a = 1 |^ d by NEWTON:10;
 b = 0 |^ d by A7, A23, NAT_1:14, NEWTON:11;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A24; ::_thesis: verum
end;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A14; ::_thesis: verum
end;
now__::_thesis:_(_a_gcd_c_=_0_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
assume  a gcd c = 0 ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A25: a = 0 by INT_2:5;
then  b = 1 by A1, NEWTON:52;
then A26: b = 1 |^ d by NEWTON:10;
 a = 0 |^ d by A7, A25, NAT_1:14, NEWTON:11;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A26; ::_thesis: verum
end;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A10; ::_thesis: verum
end;
now__::_thesis:_(_d_=_0_implies_ex_e,_f_being_Nat_st_
(_a_=_e_|^_d_&_b_=_f_|^_d_)_)
assume A27: d = 0 ; ::_thesis: ex e, f being Nat st
( a = e |^ d & b = f |^ d )
then A28: a * b = 1 by A2, NEWTON:4;
then  b divides 1 by NAT_D:def_3;
then  b = 1 by Th15;
then A29: b = 1 |^ 0 by NEWTON:4;
 a divides 1 by A28, NAT_D:def_3;
then  a = 1 by Th15;
then  a = 1 |^ 0 by NEWTON:4;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A27, A29; ::_thesis: verum
end;
hence  ex e, f being Nat st
( a = e |^ d & b = f |^ d ) by A5; ::_thesis: verum
end;

theorem Th36: :: WSIERP_1:36
for fp being FinSequence of NAT
for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) holds
(Product fp) gcd d = 1
proof
let fp be FinSequence of NAT ; ::_thesis: for d being Nat st ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) holds
(Product fp) gcd d = 1
let d be Nat; ::_thesis: ( ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 )
defpred S1[ set ] means  ex f being FinSequence of NAT st
( f = $1 & ( ( for a being Nat st a in dom f holds
(f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) );
A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_
for_a_being_Element_of_NAT_st_S1[fp]_holds_
S1[fp_^_<*a*>]
let fp be FinSequence of NAT ; ::_thesis: for a being Element of NAT st S1[fp] holds
S1[fp ^ <*a*>]
let a be Element of NAT ; ::_thesis: ( S1[fp] implies S1[fp ^ <*a*>] )
assume A2: S1[fp] ; ::_thesis: S1[fp ^ <*a*>]
thus  S1[fp ^ <*a*>] ::_thesis: verum
proof
set fp1 = fp ^ <*a*>;
take  fp ^ <*a*> ; ::_thesis: ( fp ^ <*a*> = fp ^ <*a*> & ( ( for a being Nat st a in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 ) )
thus  fp ^ <*a*> = fp ^ <*a*> ; ::_thesis: ( ( for a being Nat st a in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . a) gcd d = 1 ) implies (Product (fp ^ <*a*>)) gcd d = 1 )
assume A3: for b being Nat st b in dom (fp ^ <*a*>) holds
((fp ^ <*a*>) . b) gcd d = 1 ; ::_thesis: (Product (fp ^ <*a*>)) gcd d = 1
A4: dom fp c= dom (fp ^ <*a*>) by FINSEQ_1:26;
A5: for b being Nat st b in dom fp holds
(fp . b) gcd d = 1
proof
let b be Nat; ::_thesis: ( b in dom fp implies (fp . b) gcd d = 1 )
assume A6: b in dom fp ; ::_thesis: (fp . b) gcd d = 1
then  ((fp ^ <*a*>) . b) gcd d = 1 by A3, A4;
hence  (fp . b) gcd d = 1 by A6, FINSEQ_1:def_7; ::_thesis: verum
end;
 len (fp ^ <*a*>) in dom (fp ^ <*a*>) by FINSEQ_5:6;
then  ( len (fp ^ <*a*>) = (len fp) + 1 & ((fp ^ <*a*>) . (len (fp ^ <*a*>))) gcd d = 1 ) by A3, FINSEQ_2:16;
then A7: a gcd d = 1 by FINSEQ_1:42;
 Product (fp ^ <*a*>) = (Product fp) * a by RVSUM_1:96;
hence  (Product (fp ^ <*a*>)) gcd d = 1 by A2, A5, A7, Th6; ::_thesis: verum
end;
end;
A8: S1[ <*> NAT]
proof
take  <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds
((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) )
thus  ( <*> NAT = <*> NAT & ( ( for a being Nat st a in dom (<*> NAT) holds
((<*> NAT) . a) gcd d = 1 ) implies (Product (<*> NAT)) gcd d = 1 ) ) by NEWTON:51, RVSUM_1:94; ::_thesis: verum
end;
 for fp being FinSequence of NAT holds S1[fp] from FINSEQ_2:sch_2(A8, A1);
then  ex f being FinSequence of NAT st
( f = fp & ( ( for a being Nat st a in dom f holds
(f . a) gcd d = 1 ) implies (Product f) gcd d = 1 ) ) ;
hence  ( ( for a being Nat st a in dom fp holds
(fp . a) gcd d = 1 ) implies (Product fp) gcd d = 1 ) ; ::_thesis: verum
end;

theorem :: WSIERP_1:37
for fp being FinSequence of NAT st len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) holds
for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) )
proof
let fp be FinSequence of NAT ; ::_thesis: ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) )
defpred S1[ FinSequence of NAT ] means  for fr being FinSequence of INT st len fr = len $1 holds
ex fr1 being FinSequence of INT st
( len fr1 = len $1 & ( for b being Nat st b in dom $1 holds
(($1 . b) * (fr1 . b)) + (fr . b) = (($1 . 1) * (fr1 . 1)) + (fr . 1) ) );
defpred S2[ FinSequence of NAT ] means  for b, c being Nat st b in dom $1 & c in dom $1 & b <> c holds
($1 . b) gcd ($1 . c) = 1;
defpred S3[ set ] means  ex f being FinSequence of NAT st
( f = $1 & ( len f >= 2 & S2[f] implies S1[f] ) );
A1: now__::_thesis:_for_fp_being_FinSequence_of_NAT_
for_d_being_Element_of_NAT_st_S3[fp]_holds_
S3[fp_^_<*d*>]
let fp be FinSequence of NAT ; ::_thesis: for d being Element of NAT st S3[fp] holds
S3[fp ^ <*d*>]
let d be Element of NAT ; ::_thesis: ( S3[fp] implies S3[fp ^ <*d*>] )
assume A2: S3[fp] ; ::_thesis: S3[fp ^ <*d*>]
set k = len fp;
set fp1 = fp ^ <*d*>;
now__::_thesis:_(_len_(fp_^_<*d*>)_>=_2_&_S2[fp_^_<*d*>]_implies_S1[fp_^_<*d*>]_)
assume that
A3: len (fp ^ <*d*>) >= 2 and
A4: S2[fp ^ <*d*>] ; ::_thesis: S1[fp ^ <*d*>]
A5: len (fp ^ <*d*>) = (len fp) + 1 by FINSEQ_2:16;
now__::_thesis:_S1[fp_^_<*d*>]
percases ( len (fp ^ <*d*>) = 2 or len (fp ^ <*d*>) > 2 ) by A3, XXREAL_0:1;
supposeA6: len (fp ^ <*d*>) = 2 ; ::_thesis: S1[fp ^ <*d*>]
now__::_thesis:_for_fr_being_FinSequence_of_INT_st_len_fr_=_len_(fp_^_<*d*>)_holds_
ex_fr1_being_FinSequence_of_INT_st_
(_len_fr1_=_len_(fp_^_<*d*>)_&_(_for_b_being_Nat_st_b_in_dom_(fp_^_<*d*>)_holds_
(((fp_^_<*d*>)_._b)_*_(fr1_._b))_+_(fr_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr1_._1))_+_(fr_._1)_)_)
let fr be FinSequence of INT ; ::_thesis: ( len fr = len (fp ^ <*d*>) implies ex fr1 being FinSequence of INT st
( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) ) )
assume  len fr = len (fp ^ <*d*>) ; ::_thesis: ex fr1 being FinSequence of INT st
( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) )
 ( 1 in dom (fp ^ <*d*>) & 2 in dom (fp ^ <*d*>) ) by A6, FINSEQ_3:25;
then  ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) = 1 by A4;
then  ((fp ^ <*d*>) . 1) gcd ((fp ^ <*d*>) . 2) divides (fr . 1) - (fr . 2) by INT_2:12;
then consider m, n being Integer such that
A7: (((fp ^ <*d*>) . 1) * m) + (((fp ^ <*d*>) . 2) * n) = (fr . 1) - (fr . 2) by Th33;
reconsider x = - m, y = n as Element of INT by INT_1:def_2;
take fr1 = <*x,y*>; ::_thesis: ( len fr1 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ) )
thus  len fr1 = len (fp ^ <*d*>) by A6, FINSEQ_1:44; ::_thesis: for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
let b be Nat; ::_thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) )
assume  b in dom (fp ^ <*d*>) ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
then A8: b in Seg (len (fp ^ <*d*>)) by FINSEQ_1:def_3;
now__::_thesis:_(((fp_^_<*d*>)_._b)_*_(fr1_._b))_+_(fr_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr1_._1))_+_(fr_._1)
percases ( b = 1 or b = 2 ) by A6, A8, FINSEQ_1:2, TARSKI:def_2;
suppose b = 1 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
hence  (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; ::_thesis: verum
end;
supposeA9: b = 2 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1)
A10: ( fr1 . 1 = - m & fr1 . 2 = n ) by FINSEQ_1:44;
 (((fp ^ <*d*>) . 2) * n) - (((fp ^ <*d*>) . 1) * (- m)) = (fr . 1) - (fr . 2) by A7;
hence  (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) by A9, A10, XCMPLX_1:34; ::_thesis: verum
end;
end;
end;
hence  (((fp ^ <*d*>) . b) * (fr1 . b)) + (fr . b) = (((fp ^ <*d*>) . 1) * (fr1 . 1)) + (fr . 1) ; ::_thesis: verum
end;
hence  S1[fp ^ <*d*>] ; ::_thesis: verum
end;
supposeA11: len (fp ^ <*d*>) > 2 ; ::_thesis: S1[fp ^ <*d*>]
A12: S2[fp]
proof
A13: dom fp c= dom (fp ^ <*d*>) by FINSEQ_1:26;
let b, c be Nat; ::_thesis: ( b in dom fp & c in dom fp & b <> c implies (fp . b) gcd (fp . c) = 1 )
assume that
A14: ( b in dom fp & c in dom fp ) and
A15: b <> c ; ::_thesis: (fp . b) gcd (fp . c) = 1
 ( (fp ^ <*d*>) . b = fp . b & (fp ^ <*d*>) . c = fp . c ) by A14, FINSEQ_1:def_7;
hence  (fp . b) gcd (fp . c) = 1 by A4, A14, A15, A13; ::_thesis: verum
end;
A16: (len fp) + 1 > 1 + 1 by A11, FINSEQ_2:16;
then A17: len fp >= 1 + 1 by NAT_1:13;
now__::_thesis:_for_fr2_being_FinSequence_of_INT_st_len_fr2_=_len_(fp_^_<*d*>)_holds_
ex_fr3_being_FinSequence_of_INT_st_
(_len_fr3_=_len_(fp_^_<*d*>)_&_(_for_b_being_Nat_st_b_in_dom_(fp_^_<*d*>)_holds_
(((fp_^_<*d*>)_._b)_*_(fr3_._b))_+_(fr2_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr3_._1))_+_(fr2_._1)_)_)
let fr2 be FinSequence of INT ; ::_thesis: ( len fr2 = len (fp ^ <*d*>) implies ex fr3 being FinSequence of INT st
( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) ) )
assume A18: len fr2 = len (fp ^ <*d*>) ; ::_thesis: ex fr3 being FinSequence of INT st
( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) )
then consider fr being FinSequence of INT , m being Element of INT  such that
A19: fr2 = fr ^ <*m*> by FINSEQ_2:19;
A20: (len fp) + 1 = (len fr) + 1 by A5, A18, A19, FINSEQ_2:16;
then consider fr1 being FinSequence of INT  such that
 len fr1 = len fp and
A21: for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) by A2, A16, A12, NAT_1:13;
 for a being Nat st a in dom fp holds
(fp . a) gcd d = 1
proof
let a be Nat; ::_thesis: ( a in dom fp implies (fp . a) gcd d = 1 )
A22: (len fp) + 1 in dom (fp ^ <*d*>) by A5, FINSEQ_5:6;
A23: ( dom fp c= dom (fp ^ <*d*>) & (fp ^ <*d*>) . ((len fp) + 1) = d ) by FINSEQ_1:26, FINSEQ_1:42;
assume A24: a in dom fp ; ::_thesis: (fp . a) gcd d = 1
 (len fp) + 1 > len fp by NAT_1:13;
then A25: (len fp) + 1 <> a by A24, FINSEQ_3:25;
 (fp ^ <*d*>) . a = fp . a by A24, FINSEQ_1:def_7;
hence  (fp . a) gcd d = 1 by A4, A24, A23, A25, A22; ::_thesis: verum
end;
then  (Product fp) gcd d = 1 by Th36;
then  (Product fp) gcd d divides ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by INT_2:12;
then consider m1, n1 being Integer such that
A26: ((Product fp) * m1) + (d * n1) = ((fr2 . ((len fp) + 1)) - ((fp . 1) * (fr1 . 1))) - (fr2 . 1) by Th33;
reconsider x = - n1 as Element of INT by INT_1:def_2;
deffunc H1( Nat) ->  Element of REAL = ((Product (Del (fp,$1))) * m1) + (fr1 . $1);
consider s2 being FinSequence such that
A27: ( len s2 = len fp & ( for a being Nat st a in dom s2 holds
s2 . a = H1(a) ) ) from FINSEQ_1:sch_2();
A28: for a being Nat st a in dom s2 holds
s2 . a in INT
proof
let a be Nat; ::_thesis: ( a in dom s2 implies s2 . a in INT )
assume A29: a in dom s2 ; ::_thesis: s2 . a in INT
reconsider a = a as Element of NAT by ORDINAL1:def_12;
 s2 . a = ((Product (Del (fp,a))) * m1) + (fr1 . a) by A27, A29;
hence  s2 . a in INT by INT_1:def_2; ::_thesis: verum
end;
A30: dom s2 = Seg (len fp) by A27, FINSEQ_1:def_3;
reconsider s2 = s2 as FinSequence of INT by A28, FINSEQ_2:12;
take fr3 = s2 ^ <*x*>; ::_thesis: ( len fr3 = len (fp ^ <*d*>) & ( for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ) )
thus  len fr3 = len (fp ^ <*d*>) by A5, A27, FINSEQ_2:16; ::_thesis: for b being Nat st b in dom (fp ^ <*d*>) holds
(((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
let b be Nat; ::_thesis: ( b in dom (fp ^ <*d*>) implies (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) )
assume A31: b in dom (fp ^ <*d*>) ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
thus  (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ::_thesis: verum
proof
A32: for c being Nat st c in Seg (len fp) holds
((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c))
proof
let c be Nat; ::_thesis: ( c in Seg (len fp) implies ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c)) )
assume A33: c in Seg (len fp) ; ::_thesis: ((fp ^ <*d*>) . c) * (fr3 . c) = ((Product fp) * m1) + ((fp . c) * (fr1 . c))
then  c in dom s2 by A27, FINSEQ_1:def_3;
then A34: fr3 . c = s2 . c by FINSEQ_1:def_7
.= ((Product (Del (fp,c))) * m1) + (fr1 . c) by A27, A30, A33 ;
A35: c in dom fp by A33, FINSEQ_1:def_3;
then  fp . c = (fp ^ <*d*>) . c by FINSEQ_1:def_7;
hence ((fp ^ <*d*>) . c) * (fr3 . c) = (((fp . c) * (Product (Del (fp,c)))) * m1) + ((fp . c) * (fr1 . c)) by A34
.= ((Product fp) * m1) + ((fp . c) * (fr1 . c)) by A35, Lm16 ;
::_thesis: verum
end;
A36: b in NAT by ORDINAL1:def_12;
A37: 1 <= b by A31, FINSEQ_3:25;
A38: b <= (len fp) + 1 by A5, A31, FINSEQ_3:25;
now__::_thesis:_(((fp_^_<*d*>)_._b)_*_(fr3_._b))_+_(fr2_._b)_=_(((fp_^_<*d*>)_._1)_*_(fr3_._1))_+_(fr2_._1)
percases ( b <= len fp or b = (len fp) + 1 ) by A38, NAT_1:8;
supposeA39: b <= len fp ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
then  1 <= len fp by A37, XXREAL_0:2;
then A40: 1 in Seg (len fp) ;
then  1 in dom fr by A20, FINSEQ_1:def_3;
then A41: fr2 . 1 = fr . 1 by A19, FINSEQ_1:def_7;
A42: b in Seg (len fp) by A37, A36, A39;
then A43: b in dom fp by FINSEQ_1:def_3;
 b in dom fr by A20, A42, FINSEQ_1:def_3;
then A44: fr2 . b = fr . b by A19, FINSEQ_1:def_7;
thus (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((Product fp) * m1) + ((fp . b) * (fr1 . b))) + (fr2 . b) by A32, A42
.= ((Product fp) * m1) + (((fp . b) * (fr1 . b)) + (fr . b)) by A44
.= ((Product fp) * m1) + (((fp . 1) * (fr1 . 1)) + (fr . 1)) by A21, A43
.= (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr . 1)
.= (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A32, A40, A41 ; ::_thesis: verum
end;
supposeA45: b = (len fp) + 1 ; ::_thesis: (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1)
then A46: (fp ^ <*d*>) . b = d by FINSEQ_1:42;
A47: (fr2 . b) - (((fp . 1) * (fr1 . 1)) + (fr2 . 1)) = (d * n1) + ((Product fp) * m1) by A26, A45;
 1 <= len fp by A17, XXREAL_0:2;
then  1 in Seg (len fp) ;
then (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) = (((Product fp) * m1) + ((fp . 1) * (fr1 . 1))) + (fr2 . 1) by A32
.= (fr2 . b) + (d * (- n1)) by A47 ;
hence  (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) by A27, A45, A46, FINSEQ_1:42; ::_thesis: verum
end;
end;
end;
hence  (((fp ^ <*d*>) . b) * (fr3 . b)) + (fr2 . b) = (((fp ^ <*d*>) . 1) * (fr3 . 1)) + (fr2 . 1) ; ::_thesis: verum
end;
end;
hence  S1[fp ^ <*d*>] ; ::_thesis: verum
end;
end;
end;
hence  S1[fp ^ <*d*>] ; ::_thesis: verum
end;
hence  S3[fp ^ <*d*>] ; ::_thesis: verum
end;
A48: S3[ <*> NAT]
proof
take  <*> NAT ; ::_thesis: ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) )
thus  ( <*> NAT = <*> NAT & ( len (<*> NAT) >= 2 & S2[ <*> NAT] implies S1[ <*> NAT] ) ) ; ::_thesis: verum
end;
 for fp being FinSequence of NAT holds S3[fp] from FINSEQ_2:sch_2(A48, A1);
then  ex f being FinSequence of NAT st
( f = fp & ( len f >= 2 & S2[f] implies S1[f] ) ) ;
hence  ( len fp >= 2 & ( for b, c being Nat st b in dom fp & c in dom fp & b <> c holds
(fp . b) gcd (fp . c) = 1 ) implies for fr being FinSequence of INT st len fr = len fp holds
ex fr1 being FinSequence of INT st
( len fr1 = len fp & ( for b being Nat st b in dom fp holds
((fp . b) * (fr1 . b)) + (fr . b) = ((fp . 1) * (fr1 . 1)) + (fr . 1) ) ) ) ; ::_thesis: verum
end;

Lm17:  for k, m being Integer holds
( k divides m iff k divides abs m )
proof
let k, m be Integer; ::_thesis: ( k divides m iff k divides abs m )
percases ( m >= 0 or m < 0 ) ;
suppose m >= 0 ; ::_thesis: ( k divides m iff k divides abs m )
hence  ( k divides m iff k divides abs m ) by ABSVALUE:def_1; ::_thesis: verum
end;
suppose m < 0 ; ::_thesis: ( k divides m iff k divides abs m )
then  abs m = - m by ABSVALUE:def_1;
hence  ( k divides m iff k divides abs m ) by INT_2:10; ::_thesis: verum
end;
end;
end;

Lm18:  for m, n being Integer holds (m * n) mod n = 0
proof
let m, n be Integer; ::_thesis: (m * n) mod n = 0
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: (m * n) mod n = 0
hence (m * n) mod n = (m * n) - (((m * n) div n) * n) by INT_1:def_10
.= (m * n) - ([\((m * n) / n)/] * n) by INT_1:def_9
.= (m * n) - ([\m/] * n) by A1, XCMPLX_1:89
.= (m * n) - (m * n) by INT_1:25
.= 0 ;
::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (m * n) mod n = 0
hence  (m * n) mod n = 0 by INT_1:def_10; ::_thesis: verum
end;
end;
end;

Lm19:  for k, n, m being Integer st k mod n = m mod n holds
(k - m) mod n = 0
proof
let k, n, m be Integer; ::_thesis: ( k mod n = m mod n implies (k - m) mod n = 0 )
assume A1: k mod n = m mod n ; ::_thesis: (k - m) mod n = 0
percases ( n <> 0 or n = 0 ) ;
supposeA2: n <> 0 ; ::_thesis: (k - m) mod n = 0
then k - ((k div n) * n) = m mod n by A1, INT_1:def_10
.= m - ((m div n) * n) by A2, INT_1:def_10 ;
then  k - m = n * ((k div n) - (m div n)) ;
hence  (k - m) mod n = 0 by Lm18; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: (k - m) mod n = 0
hence  (k - m) mod n = 0 by INT_1:def_10; ::_thesis: verum
end;
end;
end;

Lm20:  for n, m being Integer st n <> 0 & m mod n = 0 holds
n divides m
proof
let n, m be Integer; ::_thesis: ( n <> 0 & m mod n = 0 implies n divides m )
assume  ( n <> 0 & m mod n = 0 ) ; ::_thesis: n divides m
then m = ((m div n) * n) + 0 by NEWTON:66
.= (m div n) * n ;
hence  n divides m by INT_1:def_3; ::_thesis: verum
end;

Lm21:  for x being Integer holds
( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) )
proof
let x be Integer; ::_thesis: ( ( 1 < x implies ( 1 < sqrt x & sqrt x < x ) ) & ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) ) )
hereby  ::_thesis: ( 0 < x & x < 1 implies ( 0 < sqrt x & sqrt x < 1 & x < sqrt x ) )
assume A1: 1 < x ; ::_thesis: ( 1 < sqrt x & sqrt x < x )
hence  1 < sqrt x by SQUARE_1:18, SQUARE_1:27; ::_thesis: sqrt x < x
then  sqrt x < (sqrt x) ^2 by SQUARE_1:14;
hence  sqrt x < x by A1, SQUARE_1:def_2; ::_thesis: verum
end;
hereby  ::_thesis: verum
assume that
A2: 0 < x and
A3: x < 1 ; ::_thesis: ( 0 < sqrt x & sqrt x < 1 & x < sqrt x )
thus A4: 0 < sqrt x by A2, SQUARE_1:17, SQUARE_1:27; ::_thesis: ( sqrt x < 1 & x < sqrt x )
thus  sqrt x < 1 by A2, A3, SQUARE_1:18, SQUARE_1:27; ::_thesis: x < sqrt x
then  (sqrt x) ^2 < sqrt x by A4, SQUARE_1:13;
hence  x < sqrt x by A2, SQUARE_1:def_2; ::_thesis: verum
end;
end;

theorem :: WSIERP_1:38
for a being Nat
for k being Integer st a <> 0 & a gcd k = 1 holds
ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
proof
let a be Nat; ::_thesis: for k being Integer st a <> 0 & a gcd k = 1 holds
ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
let k be Integer; ::_thesis: ( a <> 0 & a gcd k = 1 implies ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) ) )
assume that
A1: a <> 0 and
A2: a gcd k = 1 ; ::_thesis: ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
A3: a >= 1 by A1, NAT_1:14;
percases ( a = 1 or a > 1 ) by A3, XXREAL_0:1;
supposeA4: a = 1 ; ::_thesis: ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
take b = 1; ::_thesis: ex e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
take e = 1; ::_thesis: ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
thus  ( b <> 0 & e <> 0 ) ; ::_thesis: ( b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
thus  ( b <= sqrt a & e <= sqrt a ) by A4, SQUARE_1:18; ::_thesis: ( a divides (k * b) + e or a divides (k * b) - e )
thus  ( a divides (k * b) + e or a divides (k * b) - e ) by A4, INT_2:12; ::_thesis: verum
end;
supposeA5: a > 1 ; ::_thesis: ex b, e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
A6: sqrt a > 0 by A1, SQUARE_1:25;
set d = [\(sqrt a)/];
A7: [\(sqrt a)/] <= sqrt a by INT_1:def_6;
 sqrt a < a by A5, Lm21;
then A8: [\(sqrt a)/] < a by A7, XXREAL_0:2;
set d1 = [\(sqrt a)/] + 1;
A9: [\(sqrt a)/] > (sqrt a) - 1 by INT_1:def_6;
 sqrt a > 1 by A5, SQUARE_1:18, SQUARE_1:27;
then A10: (sqrt a) - 1 > 0 by XREAL_1:50;
then reconsider d = [\(sqrt a)/] as Element of NAT by A9, INT_1:3;
A11: d + 1 >= 1 by Lm1;
then reconsider d1 = [\(sqrt a)/] + 1 as Element of NAT ;
set e1 = d1 ^2 ;
 d1 ^2 = d1 * d1 ;
then reconsider e1 = d1 ^2 as Element of NAT ;
A12: (e1 - 1) / d1 = d1 - (1 / d1) by A11, XCMPLX_1:127;
deffunc H1( Nat) ->  Element of REAL = 1 + (((k * (($1 - 1) div d1)) + (($1 - 1) mod d1)) mod a);
consider fs being FinSequence such that
A13: ( len fs = e1 & ( for b being Nat st b in dom fs holds
fs . b = H1(b) ) ) from FINSEQ_1:sch_2();
A14: rng fs c= Seg a
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng fs or v in Seg a )
assume  v in rng fs ; ::_thesis: v in Seg a
then consider b being Nat such that
A15: ( b in dom fs & fs . b = v ) by FINSEQ_2:10;
A16: v = 1 + (((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a) by A13, A15;
then reconsider v1 = v as Integer ;
A17: 0 <= ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a by NEWTON:64;
then A18: 1 <= v1 by A16, Lm1;
reconsider v1 = v1 as Element of NAT by A16, A17, INT_1:3;
 ((k * ((b - 1) div d1)) + ((b - 1) mod d1)) mod a < a by A1, NEWTON:65;
then  v1 <= a by A16, Lm9;
hence  v in Seg a by A18; ::_thesis: verum
end;
 sqrt a < d1 by A9, XREAL_1:19;
then  (sqrt a) ^2 < e1 by A6, SQUARE_1:16;
then A19: a < e1 by SQUARE_1:def_2;
then A20: Seg a c= Seg e1 by FINSEQ_1:5;
A21: Seg e1 = dom fs by A13, FINSEQ_1:def_3;
then  rng fs <> dom fs by A19, A14, FINSEQ_1:5;
then  not fs is one-to-one by A21, A14, A20, FINSEQ_4:59, XBOOLE_1:1;
then consider v1, v2 being set  such that
A22: v1 in dom fs and
A23: v2 in dom fs and
A24: fs . v1 = fs . v2 and
A25: v1 <> v2 by FUNCT_1:def_4;
reconsider v1 = v1, v2 = v2 as Element of NAT by A22, A23;
set x1 = (v1 - 1) div d1;
set x2 = (v2 - 1) div d1;
set x = ((v1 - 1) div d1) - ((v2 - 1) div d1);
set y1 = (v1 - 1) mod d1;
set y2 = (v2 - 1) mod d1;
set y = ((v1 - 1) mod d1) - ((v2 - 1) mod d1);
A26: (v1 - 1) mod d1 >= 0 by NEWTON:64;
 ( fs . v1 = 1 + (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) mod a) & fs . v2 = 1 + (((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) mod a) ) by A13, A22, A23;
then A27: (((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1))) mod a = 0 by A24, Lm19, XCMPLX_1:2;
then A28: a divides ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) by A1, Lm20;
 1 / d1 > 0 by A9, A10, XREAL_1:139;
then A29: (e1 - 1) / d1 < d1 by A12, Lm1;
A30: (v2 - 1) div d1 = [\((v2 - 1) / d1)/] by INT_1:def_9;
then A31: (v2 - 1) div d1 <= (v2 - 1) / d1 by INT_1:def_6;
 v2 <= e1 by A13, A23, FINSEQ_3:25;
then  v2 - 1 <= e1 - 1 by XREAL_1:9;
then  (v2 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72;
then  (v2 - 1) / d1 < d1 by A29, XXREAL_0:2;
then  (v2 - 1) div d1 < d1 by A31, XXREAL_0:2;
then A32: (v2 - 1) div d1 <= d by Lm9;
set d2 = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1));
A33: [\0/] = 0 by INT_1:25;
A34: (v1 - 1) div d1 = [\((v1 - 1) / d1)/] by INT_1:def_9;
then A35: (v1 - 1) div d1 <= (v1 - 1) / d1 by INT_1:def_6;
 1 <= v1 by A22, FINSEQ_3:25;
then  v1 - 1 >= 0 by XREAL_1:48;
then  (v1 - 1) div d1 >= 0 by A34, A33, PRE_FF:9;
then  ((v2 - 1) div d1) - ((v1 - 1) div d1) <= d by A32, Lm2;
then A36: - (((v2 - 1) div d1) - ((v1 - 1) div d1)) >= - d by XREAL_1:24;
A37: ( ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 or ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 )
proof
assume  ( not ((v1 - 1) div d1) - ((v2 - 1) div d1) <> 0 & not ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <> 0 ) ; ::_thesis: contradiction
then v1 - 1 = (((v2 - 1) div d1) * d1) + ((v2 - 1) mod d1) by A11, NEWTON:66
.= v2 - 1 by A11, NEWTON:66 ;
hence  contradiction by A25; ::_thesis: verum
end;
 v1 <= e1 by A13, A22, FINSEQ_3:25;
then  v1 - 1 <= e1 - 1 by XREAL_1:9;
then  (v1 - 1) / d1 <= (e1 - 1) / d1 by XREAL_1:72;
then  (v1 - 1) / d1 < d1 by A29, XXREAL_0:2;
then  (v1 - 1) div d1 < d1 by A35, XXREAL_0:2;
then A38: (v1 - 1) div d1 <= d by Lm9;
A39: ((k * ((v1 - 1) div d1)) + ((v1 - 1) mod d1)) - ((k * ((v2 - 1) div d1)) + ((v2 - 1) mod d1)) = (k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ;
 (v2 - 1) mod d1 < d1 by A9, A10, NEWTON:65;
then  ((v2 - 1) mod d1) - ((v1 - 1) mod d1) < d1 by A26, Lm3;
then  ((v2 - 1) mod d1) - ((v1 - 1) mod d1) <= d by Lm9;
then A40: - (((v2 - 1) mod d1) - ((v1 - 1) mod d1)) >= - d by XREAL_1:24;
take b = abs (((v1 - 1) div d1) - ((v2 - 1) div d1)); ::_thesis: ex e being Nat st
( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
take e = abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)); ::_thesis: ( 0 <> b & 0 <> e & b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
A41: (v2 - 1) mod d1 >= 0 by NEWTON:64;
 1 <= v2 by A23, FINSEQ_3:25;
then  v2 - 1 >= 0 by XREAL_1:48;
then  (v2 - 1) div d1 >= 0 by A30, A33, PRE_FF:9;
then  ((v1 - 1) div d1) - ((v2 - 1) div d1) <= d by A38, Lm2;
then A42: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) <= d by A36, ABSVALUE:5;
then A43: abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) < a by A8, XXREAL_0:2;
A44: now__::_thesis:_not_((v1_-_1)_mod_d1)_-_((v2_-_1)_mod_d1)_=_0
assume A45: ((v1 - 1) mod d1) - ((v2 - 1) mod d1) = 0 ; ::_thesis: contradiction
then  a divides ((v1 - 1) div d1) - ((v2 - 1) div d1) by A1, A2, A27, A39, Lm20, Th29;
then  a divides abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) by Lm17;
then  abs (((v1 - 1) div d1) - ((v2 - 1) div d1)) = 0 by A43, NAT_D:7;
hence  contradiction by A37, A45, ABSVALUE:2; ::_thesis: verum
end;
 (v1 - 1) mod d1 < d1 by A9, A10, NEWTON:65;
then  ((v1 - 1) mod d1) - ((v2 - 1) mod d1) < d1 by A41, Lm3;
then  ((v1 - 1) mod d1) - ((v2 - 1) mod d1) <= d by Lm9;
then A46: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) <= d by A40, ABSVALUE:5;
then A47: abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) < a by A8, XXREAL_0:2;
now__::_thesis:_not_((v1_-_1)_div_d1)_-_((v2_-_1)_div_d1)_=_0
assume A48: ((v1 - 1) div d1) - ((v2 - 1) div d1) = 0 ; ::_thesis: contradiction
then  a divides abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) by A28, Lm17;
then  abs (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) = 0 by A47, NAT_D:7;
hence  contradiction by A37, A48, ABSVALUE:2; ::_thesis: verum
end;
hence  ( b <> 0 & e <> 0 ) by A44, ABSVALUE:2; ::_thesis: ( b <= sqrt a & e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
thus  b <= sqrt a by A7, A42, XXREAL_0:2; ::_thesis: ( e <= sqrt a & ( a divides (k * b) + e or a divides (k * b) - e ) )
thus  e <= sqrt a by A7, A46, XXREAL_0:2; ::_thesis: ( a divides (k * b) + e or a divides (k * b) - e )
A49: ( b = ((v1 - 1) div d1) - ((v2 - 1) div d1) or b = - (((v1 - 1) div d1) - ((v2 - 1) div d1)) ) by ABSVALUE:1;
A50: ( e = ((v1 - 1) mod d1) - ((v2 - 1) mod d1) or e = - (((v1 - 1) mod d1) - ((v2 - 1) mod d1)) ) by ABSVALUE:1;
 - ((k * (((v1 - 1) div d1) - ((v2 - 1) div d1))) + (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) = (k * (- (((v1 - 1) div d1) - ((v2 - 1) div d1)))) + (- (((v1 - 1) mod d1) - ((v2 - 1) mod d1))) ;
hence  ( a divides (k * b) + e or a divides (k * b) - e ) by A28, A49, A50, INT_2:10; ::_thesis: verum
end;
end;
end;

theorem :: WSIERP_1:39
for a being Nat
for fs being FinSequence holds dom (Del (fs,a)) c= dom fs by Lm12;

theorem :: WSIERP_1:40
for fs being FinSequence
for v being set holds
( Del ((<*v*> ^ fs),1) = fs & Del ((fs ^ <*v*>),((len fs) + 1)) = fs ) by Lm14;

begin

theorem :: WSIERP_1:41
for k being Integer
for n being Nat st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1
proof
let k be Integer; ::_thesis: for n being Nat st n > 0 & k mod n <> 0 holds
- (k div n) = ((- k) div n) + 1
let n be Nat; ::_thesis: ( n > 0 & k mod n <> 0 implies - (k div n) = ((- k) div n) + 1 )
assume A1: n > 0 ; ::_thesis: ( not k mod n <> 0 or - (k div n) = ((- k) div n) + 1 )
assume  k mod n <> 0 ; ::_thesis: - (k div n) = ((- k) div n) + 1
then  not n divides k by A1, INT_1:62;
then A2: k / n is not Integer by A1, Th17;
thus  - (k div n) = - [\(k / n)/] by INT_1:def_9
.= [\((- k) / n)/] + 1 by A2, INT_1:63
.= ((- k) div n) + 1 by INT_1:def_9 ; ::_thesis: verum
end;

theorem :: WSIERP_1:42
for k being Integer
for n being Nat st n > 0 & k mod n = 0 holds
- (k div n) = (- k) div n
proof
let k be Integer; ::_thesis: for n being Nat st n > 0 & k mod n = 0 holds
- (k div n) = (- k) div n
let n be Nat; ::_thesis: ( n > 0 & k mod n = 0 implies - (k div n) = (- k) div n )
assume A1: n > 0 ; ::_thesis: ( not k mod n = 0 or - (k div n) = (- k) div n )
assume  k mod n = 0 ; ::_thesis: - (k div n) = (- k) div n
then  n divides k by A1, INT_1:62;
then A2: k / n is Integer by A1, Th17;
thus  - (k div n) = - [\(k / n)/] by INT_1:def_9
.= [\((- k) / n)/] by A2, INT_1:64
.= (- k) div n by INT_1:def_9 ; ::_thesis: verum
end;