deffunc H₁( 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₁(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