let p1, p2 be Element of the carrier of L * ; :: 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)) ) & len p2 = len t & ( for k being Element of NAT st k in dom t holds
p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ) implies p1 = p2 )
assume that
A4: len p1 = len t and
A5: 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)) and
A6: len p2 = len t and
A7: for k being Element of NAT st k in dom t holds
p2 . k = ((p . ((t /. k) /. 1)) * (q . ((t /. k) /. 2))) * (r . ((t /. k) /. 3)) ; :: thesis: p1 = p2
A8: dom p1 = Seg (len t) by A4, FINSEQ_1:def 3;
now :: thesis: for i being Nat st i in dom p1 holds
p1 . i = p2 . i
let i be Nat; :: thesis: ( i in dom p1 implies p1 . i = p2 . i )
assume i in dom p1 ; :: thesis: p1 . i = p2 . i
then A9: i in dom t by A8, FINSEQ_1:def 3;
hence p1 . i = ((p . ((t /. i) /. 1)) * (q . ((t /. i) /. 2))) * (r . ((t /. i) /. 3)) by A5
.= p2 . i by A7, A9 ;
:: thesis: verum
end;
hence p1 = p2 by A4, A6, FINSEQ_2:9; :: thesis: verum