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

let n be Nat; :: thesis:
assume A35: S₁[n] ; :: thesis:
assume (n + 1) + 1 <= len F ; :: thesis:
then A36: n + 1 < len F by NAT_1:13;
then f2 . (n + 1) = b . ((f2 . n),(F . (n + 1))) by A32;
hence f1 . (n + 1) = f2 . (n + 1) by A29, A35, A36; :: thesis:

end;