deffunc H_{1}( Nat) -> Element of the carrier of L = ((p . ((t /. $1) /. 1)) * (q . ((t /. $1) /. 2))) * (r . ((t /. $1) /. 3));

consider p1 being FinSequence of the carrier of L such that

A1: len p1 = len t and

A2: for k being Nat st k in dom p1 holds

p1 . k = H_{1}(k)
from FINSEQ_2:sch 1();

A3: dom p1 = Seg (len t) by A1, FINSEQ_1:def 3;

reconsider p1 = p1 as Element of the carrier of L * by FINSEQ_1:def 11;

take p1 ; :: thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds

p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )

thus len p1 = len t by A1; :: thesis: for k being Element of NAT st k in dom t holds

p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))

let k be Element of NAT ; :: thesis: ( k in dom t implies p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) )

assume k in dom t ; :: thesis: p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))

then k in Seg (len t) by FINSEQ_1:def 3;

hence p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) by A2, A3; :: thesis: verum

consider p1 being FinSequence of the carrier of L such that

A1: len p1 = len t and

A2: for k being Nat st k in dom p1 holds

p1 . k = H

A3: dom p1 = Seg (len t) by A1, FINSEQ_1:def 3;

reconsider p1 = p1 as Element of the carrier of L * by FINSEQ_1:def 11;

take p1 ; :: thesis: ( len p1 = len t & ( for k being Element of NAT st k in dom t holds

p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) )

thus len p1 = len t by A1; :: thesis: for k being Element of NAT st k in dom t holds

p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))

let k be Element of NAT ; :: thesis: ( k in dom t implies p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) )

assume k in dom t ; :: thesis: p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3))

then k in Seg (len t) by FINSEQ_1:def 3;

hence p1 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) by A2, A3; :: thesis: verum