deffunc H₁( 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₁(k) ) ) from FINSEQ_2:sch 1();
dom F1 = dom F by A1, FINSEQ_3:29;
hence ex b₁ being FinSequence of the carrier of G st
( len b₁ = len F & ( for k being Nat st k in dom F holds
b₁ . k = (F /. k) |^ a ) ) by A1; :: thesis: verum