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 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 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 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 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 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 Nat st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) )

assume A1: ( 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 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 Nat st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1)

defpred S1[ 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) ) );
A2: S1[ 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 A1
.= (0 * x) + (1 * y) by A1
.= g . (I0 + 1) by A1 ;
hence ( ((a . 0) * x) + ((b . 0) * y) = g . 0 & ((a . (0 + 1)) * x) + ((b . (0 + 1)) * y) = g . (0 + 1) ) by A1; :: thesis: verum
end;
A3: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[i + 1]
assume A5: 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) )
A6: w . i <> 0
proof
assume A7: w . i = 0 ; :: thesis: contradiction
t . (i + 1) = (g . i) mod (w . i) by A1
.= 0 by ;
hence contradiction by A1, A5; :: thesis: verum
end;
((a . ((i + 1) + 1)) * x) + ((b . ((i + 1) + 1)) * y) = ((u . (i + 1)) * x) + ((b . ((i + 1) + 1)) * y) by A1
.= ((u . (i + 1)) * x) + ((v . (i + 1)) * y) by A1
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + ((v . (i + 1)) * y) by A1
.= (((a . i) - ((q . (i + 1)) * (u . i))) * x) + (((b . i) - ((q . (i + 1)) * (v . i))) * y) by A1
.= (g . i) - ((q . (i + 1)) * (((u . i) * x) + ((v . i) * y))) by A6, A4
.= (g . i) - ((q . (i + 1)) * (((a . (i + 1)) * x) + ((v . i) * y))) by A1
.= (g . i) - ((q . (i + 1)) * (g . (i + 1))) by A6, A4, A1
.= (g . i) - (((g . i) div (w . i)) * (g . (i + 1))) by A1
.= (g . i) - (((g . i) div (w . i)) * (w . i)) by A1
.= (g . i) mod (w . i) by
.= t . (i + 1) by A1
.= w . (i + 1) by A1
.= g . ((i + 1) + 1) by A1 ;
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 A6, A4; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A2, A3);
hence for i being Nat st w . i <> 0 holds
((a . (i + 1)) * x) + ((b . (i + 1)) * y) = g . (i + 1) ; :: thesis: verum