defpred S₁[ Nat, Function of L,L, Function of L,L] means $3 = $2 * f;
A: for n being Nat
for g1 being Function of L,L ex g2 being Function of L,L st S₁[n,g1,g2] ;
consider F being Funcs (L,L) -valued sequence such that
B: ( F . 0 = id L & ( for n being Nat holds S₁[n,F . n,F . (n + 1)] ) ) from FIELD_16:sch 1(A);
take F . n ; :: thesis: ex F being Funcs (L,L) -valued sequence st
( F . n = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) )
take F ; :: thesis: ( F . n = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) )
thus ( F . n = F . n & F . 0 = id L & ( for i being Nat holds F . (i + 1) = (F . i) * f ) ) by B; :: thesis: verum