let x, y be Element of INT ; :: thesis: for g, w, q, t, a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds
for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
let g, w, q, t be sequence of INT; :: thesis: for a, b, v, u being sequence of INT st a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) holds
for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
let a, b, v, u be sequence of INT; :: thesis: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) implies for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) )
assume AS: ( a . 0 = 1 & b . 0 = 0 & g . 0 = x & q . 0 = 0 & u . 0 = 0 & v . 0 = 1 & w . 0 = y & t . 0 = 0 & ( for i being Element of NAT holds
( q . (i + 1) = (g . i) div (w . i) & t . (i + 1) = (g . i) mod (w . i) & a . (i + 1) = u . i & b . (i + 1) = v . i & g . (i + 1) = w . i & u . (i + 1) = (a . i) - ((q . (i + 1)) * (u . i)) & v . (i + 1) = (b . i) - ((q . (i + 1)) * (v . i)) & w . (i + 1) = t . (i + 1) ) ) ) ; :: thesis: for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)
defpred S₁[ Nat] means ( w . $1 <> 0 implies ( ((a . $1) * x) + ((b . $1) * y) = g . $1 & ((a . ($1 + 1)) * x) + ((b . ($1 + 1)) * y) = g . ($1 + 1) ) );
P0: S₁[ 0 ]

proof

assume w . 0 <> 0 ; :: thesis: ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) )
reconsider I0 = 0 as Element of NAT ;
((a . (I0 + 1)) * x) + ((b . (I0 + 1)) * y) = ((u . 0) * x) + ((b . (I0 + 1)) * y) by AS
.= (0 * x) + (1 * y) by AS
.= g . (I0 + 1) by AS ;
hence ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) ) by AS; :: thesis: verum

end;

P1: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume P12A: S₁[i] ; :: thesis: S₁[i + 1]
assume ASX: w . (i + 1) <> 0 ; :: thesis: ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) )
XX1: w . i <> 0

proof

assume XX2: w . i = 0 ; :: thesis: contradiction
t . (i + 1) = (g . i) mod (w . i) by AS
.= 0 by XX2, INT_1:def 10 ;
hence contradiction by AS, ASX; :: thesis: verum

end;

((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = ((u . (i + 1)) * x) + ((b . ((i + 1) + 1)) * y) by AS
.= ((u . (i + 1)) * x) + ((v . (i + 1)) * y) by AS
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + ((v . (i + 1)) * y) by AS
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + (((b . i) - ((q . (i + 1)) * (v . i))) * y) by AS
.= (g . i) - ((q . (i + 1)) * (((u . i) * x) + ((v . i) * y))) by XX1, P12A
.= (g . i) - ((q . (i + 1)) * (((a . (i + 1)) * x) + ((v . i) * y))) by AS
.= (g . i) - ((q . (i + 1)) * (g . (i + 1))) by XX1, P12A, AS
.= (g . i) - (((g . i) div (w . i)) * (g . (i + 1))) by AS
.= (g . i) - (((g . i) div (w . i)) * (w . i)) by AS
.= (g . i) mod (w . i) by INT_1:def 10, XX1
.= t . (i + 1) by AS
.= w . (i + 1) by AS
.= g . ((i + 1) + 1) by AS ;
hence ( ((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) & ((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = g . ((i + 1) + 1) ) by XX1, P12A; :: thesis: verum

end;

for i being Element of NAT holds S₁[i] from NAT_1:sch 1(P0, P1);
hence for i being Element of NAT st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) ; :: thesis: verum