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;

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

hence
p1 = p2
by A4, A6, FINSEQ_2:9; :: thesis: verump1 . 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;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