deffunc H1( 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 = H1(k) from A3: dom p1 = Seg (len t) by ;
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