deffunc H₁( set ) -> Element of the carrier of L = (p /. $1) * a;
consider f being FinSequence of the carrier of L such that
A1: len f = len p and
A2: for j being Nat st j in dom f holds
f /. j = H₁(j) from FINSEQ_4:sch 2();
take f ; :: thesis: ( dom f = dom p & ( for i being set st i in dom p holds
f /. i = (p /. i) * a ) )
thus A3: dom f = dom p by A1, FINSEQ_3:29; :: thesis: for i being set st i in dom p holds
f /. i = (p /. i) * a
let j be set ; :: thesis: ( j in dom p implies f /. j = (p /. j) * a )
assume j in dom p ; :: thesis: f /. j = (p /. j) * a
hence f /. j = (p /. j) * a by A2, A3; :: thesis: verum