let f1, f2 be Function of L,L; :: thesis: ( ex F being Funcs (L,L) -valued sequence st
( f1 = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) & ex F being Funcs (L,L) -valued sequence st
( f2 = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) implies f1 = f2 )
given F1 being Funcs (L,L) -valued sequence such that A: ( f1 = F1 . n & F1 . 0 = id L & ( for i being Nat holds F1 . (i + 1) = (F1 . i) * f ) ) ; :: thesis: ( for F being Funcs (L,L) -valued sequence holds
( not f2 = F . n or not F . 0 = id L or ex i being Nat st not F . (i + 1) = (F . i) * f ) or f1 = f2 )
given F2 being Funcs (L,L) -valued sequence such that B: ( f2 = F2 . n & F2 . 0 = id L & ( for i being Nat holds F2 . (i + 1) = (F2 . i) * f ) ) ; :: thesis: f1 = f2
defpred S₁[ Nat] means F1 . $1 = F2 . $1;
IA: S₁[ 0 ] by A, B;

IS: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then F1 . (k + 1) = (F2 . k) * f by A
.= F2 . (k + 1) by B ;
hence S₁[k + 1] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(IA, IS);
hence f1 = f2 by A, B; :: thesis: verum