deffunc H₁( Nat) -> Element of the carrier of L = ((B * E) . $1) * (E /. $1);
consider z being FinSequence of L such that
A1: ( len z = len E & ( for j being Nat st j in dom z holds
z . j = H₁(j) ) ) from FINSEQ_2:sch 1();
take z ; :: thesis: ( len z = len E & ( for n being Nat st 1 <= n & n <= len z holds
z . n = ((B * E) . n) * (E /. n) ) )
thus ( len z = len E & ( for n being Nat st 1 <= n & n <= len z holds
z . n = ((B * E) . n) * (E /. n) ) ) by A1, FINSEQ_3:25; :: thesis: verum