A: for x being Element of U * holds H₁(x) is Element of U * by FINSEQ_1:def 11;
consider f being Function of (U *),(U *) such that
B0: for x being Element of U * holds f . x = H₁(x) from FUNCT_2:sch 9(A);
take f ; :: thesis: for q being U -valued FinSequence holds f . q = (x,u) -SymbolSubstIn q

now

let q be U -valued FinSequence; :: thesis: f . q = (x,u) -SymbolSubstIn q
reconsider qq = q as FinSequence of U by Lm45;
reconsider qqq = qq as Element of U * by FINSEQ_1:def 11;
f . qqq = H₁(qqq) by B0;
hence f . q = (x,u) -SymbolSubstIn q ; :: thesis: verum

end;

hence for q being U -valued FinSequence holds f . q = (x,u) -SymbolSubstIn q ; :: thesis: verum