deffunc H_{1}( Nat) -> Element of the carrier of G = (F /. $1) |^ a;

consider F1 being FinSequence of the carrier of G such that

A1: ( len F1 = len F & ( for k being Nat st k in dom F1 holds

F1 . k = H_{1}(k) ) )
from FINSEQ_2:sch 1();

dom F1 = dom F by A1, FINSEQ_3:29;

hence ex b_{1} being FinSequence of the carrier of G st

( len b_{1} = len F & ( for k being Nat st k in dom F holds

b_{1} . k = (F /. k) |^ a ) )
by A1; :: thesis: verum

consider F1 being FinSequence of the carrier of G such that

A1: ( len F1 = len F & ( for k being Nat st k in dom F1 holds

F1 . k = H

dom F1 = dom F by A1, FINSEQ_3:29;

hence ex b

( len b

b