let m1, m2 be Element of NAT ; :: thesis: ( ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m1 = A . (min* { i where i is Nat : B . i = 0 } ) ) & ex A, B being sequence of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m2 = A . (min* { i where i is Nat : B . i = 0 } ) ) implies m1 = m2 )
given A1, B1 being sequence of NAT such that A2: ( A1 . 0 = |.a.| & B1 . 0 = |.b.| & ( for i being Nat holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Nat : B1 . i = 0 } ) ) ; :: thesis: ( for A, B being sequence of NAT holds
( not A . 0 = |.a.| or not B . 0 = |.b.| or ex i being Nat st
( A . (i + 1) = B . i implies not B . (i + 1) = (A . i) mod (B . i) ) or not m2 = A . (min* { i where i is Nat : B . i = 0 } ) ) or m1 = m2 )
assume ex A2, B2 being sequence of NAT st
( A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Nat : B2 . i = 0 } ) ) ; :: thesis: m1 = m2
then consider A2, B2 being sequence of NAT such that
A3: ( A2 . 0 = |.a.| & B2 . 0 = |.b.| & ( for i being Nat holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Nat : B2 . i = 0 } ) ) ;
( A1 = A2 & B1 = B2 ) by Lm2, A2, A3;
hence m1 = m2 by A2, A3; :: thesis: verum