deffunc H_{1}( Nat, Element of Funcs (X,X)) -> Element of Funcs (X,X) = f * $2;

let F1, F2 be sequence of (Funcs (X,X)); :: thesis: ( F1 . 0 = id X & ( for i being Nat holds F1 . (i + 1) = f * (F1 . i) ) & F2 . 0 = id X & ( for i being Nat holds F2 . (i + 1) = f * (F2 . i) ) implies F1 = F2 )

assume that

A1: F1 . 0 = id X and

A2: for i being Nat holds F1 . (i + 1) = H_{1}(i,F1 . i)
and

A3: F2 . 0 = id X and

A4: for i being Nat holds F2 . (i + 1) = H_{1}(i,F2 . i)
; :: thesis: F1 = F2

thus F1 = F2 from NAT_1:sch 16(A1, A2, A3, A4); :: thesis: verum

let F1, F2 be sequence of (Funcs (X,X)); :: thesis: ( F1 . 0 = id X & ( for i being Nat holds F1 . (i + 1) = f * (F1 . i) ) & F2 . 0 = id X & ( for i being Nat holds F2 . (i + 1) = f * (F2 . i) ) implies F1 = F2 )

assume that

A1: F1 . 0 = id X and

A2: for i being Nat holds F1 . (i + 1) = H

A3: F2 . 0 = id X and

A4: for i being Nat holds F2 . (i + 1) = H

thus F1 = F2 from NAT_1:sch 16(A1, A2, A3, A4); :: thesis: verum