consider f being Function of (U *),(U *) such that
A1: for x being Element of U * holds f . x = H₁(x) from FUNCT_2:sch 4();
take f ; :: thesis: for q being U -valued FinSequence holds f . q = (x,u) -SymbolSubstIn q

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

let q be U -valued FinSequence; :: thesis: f . q = (x,u) -SymbolSubstIn q
reconsider qq = q as FinSequence of U by Lm1;
reconsider qqq = qq as Element of U * ;
f . qqq = H₁(qqq) by A1;
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