let m1, m2 be Element of NAT ; :: thesis: ( ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m1 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) & ex A, B being sequence of NAT st
( A . 0 = abs a & B . 0 = abs b & ( for i being Element of NAT holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & m2 = A . (min* { i where i is Element of NAT : B . i = 0 } ) ) implies m1 = m2 )
assume ex A1, B1 being sequence of NAT st
( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ; :: thesis: ( for A, B being sequence of NAT holds
( not A . 0 = abs a or not B . 0 = abs b or ex i being Element of 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 Element of NAT : B . i = 0 } ) ) or m1 = m2 )
then consider A1, B1 being sequence of NAT such that
P1: ( A1 . 0 = abs a & B1 . 0 = abs b & ( for i being Element of NAT holds
( A1 . (i + 1) = B1 . i & B1 . (i + 1) = (A1 . i) mod (B1 . i) ) ) & m1 = A1 . (min* { i where i is Element of NAT : B1 . i = 0 } ) ) ;
assume ex A2, B2 being sequence of NAT st
( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ; :: thesis: m1 = m2
then consider A2, B2 being sequence of NAT such that
P2: ( A2 . 0 = abs a & B2 . 0 = abs b & ( for i being Element of NAT holds
( A2 . (i + 1) = B2 . i & B2 . (i + 1) = (A2 . i) mod (B2 . i) ) ) & m2 = A2 . (min* { i where i is Element of NAT : B2 . i = 0 } ) ) ;
( A1 = A2 & B1 = B2 ) by LM2, P1, P2;
hence m1 = m2 by P1, P2; :: thesis: verum