let d1, d2 be Element of D; :: thesis: ( ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) & ( ( not g is having_a_unity or not len F = 0 ) & ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 ) )
thus ( g is having_a_unity & len F = 0 & d1 = the_unity_wrt g & d2 = the_unity_wrt g implies d1 = d2 ) ; :: thesis: ( ( not g is having_a_unity or not len F = 0 ) & ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d1 = f . (len F) ) & ex f being sequence of D st
( f . 1 = F . 1 & ( for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) ) & d2 = f . (len F) ) implies d1 = d2 )
assume A27: ( not g is having_a_unity or len F <> 0 ) ; :: thesis: ( for f being sequence of D holds
( not f . 1 = F . 1 or ex n being Nat st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d1 = f . (len F) ) or for f being sequence of D holds
( not f . 1 = F . 1 or ex n being Nat st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 )
given f1 being sequence of D such that A28: f1 . 1 = F . 1 and
A29: for n being Nat st 0 <> n & n < len F holds
f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) and
A30: d1 = f1 . (len F) ; :: thesis: ( for f being sequence of D holds
( not f . 1 = F . 1 or ex n being Nat st
( 0 <> n & n < len F & not f . (n + 1) = g . ((f . n),(F . (n + 1))) ) or not d2 = f . (len F) ) or d1 = d2 )
given f2 being sequence of D such that A31: f2 . 1 = F . 1 and
A32: for n being Nat st 0 <> n & n < len F holds
f2 . (n + 1) = g . ((f2 . n),(F . (n + 1))) and
A33: d2 = f2 . (len F) ; :: thesis: d1 = d2
defpred S₁[ Nat] means ( $1 <> 0 & $1 <= len F implies f1 . $1 = f2 . $1 );
A34: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A35: ( n <> 0 & n <= len F implies f1 . n = f2 . n ) ; :: thesis: S₁[n + 1]
assume that
n + 1 <> 0 and
A36: n + 1 <= len F ; :: thesis: f1 . (n + 1) = f2 . (n + 1)

now :: thesis: f1 . (n + 1) = f2 . (n + 1)

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: f1 . (n + 1) = f2 . (n + 1)

hence f1 . (n + 1) = f2 . (n + 1) by A28, A31; :: thesis: verum

end;

suppose A37: n <> 0 ; :: thesis: f1 . (n + 1) = f2 . (n + 1)

A38: n < len F by A36, NAT_1:13;
then f1 . (n + 1) = g . ((f1 . n),(F . (n + 1))) by A29, A37;
hence f1 . (n + 1) = f2 . (n + 1) by A32, A35, A37, A38; :: thesis: verum

end;

end;

end;

hence f1 . (n + 1) = f2 . (n + 1) ; :: thesis: verum

end;

A39: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A39, A34);
hence d1 = d2 by A1, A27, A30, A33; :: thesis: verum