let it1, it2 be FinSequence of the carrier of L; :: thesis: ( dom it1 = dom p & ( for i being object st i in dom p holds
it1 /. i = (p /. i) * a ) & dom it2 = dom p & ( for i being object st i in dom p holds
it2 /. i = (p /. i) * a ) implies it1 = it2 )
assume that
A4: dom it1 = dom p and
A5: for i being object st i in dom p holds
it1 /. i = (p /. i) * a and
A6: dom it2 = dom p and
A7: for i being object st i in dom p holds
it2 /. i = (p /. i) * a ; :: thesis: it1 = it2

now :: thesis: for j being Nat st j in dom p holds
it1 /. j = it2 /. j

let j be Nat; :: thesis: ( j in dom p implies it1 /. j = it2 /. j )
assume A8: j in dom p ; :: thesis: it1 /. j = it2 /. j
hence it1 /. j = (p /. j) * a by A5
.= it2 /. j by A7, A8 ;
:: thesis: verum

end;

hence it1 = it2 by A4, A6, FINSEQ_5:12; :: thesis: verum