let T1, T2 be FinSequence_of_Matrix of K; :: thesis: ( dom T1 = dom G & ( for i being Nat st i in dom T1 holds
T1 . i = (p /. i) * (G . i) ) & dom T2 = dom G & ( for i being Nat st i in dom T2 holds
T2 . i = (p /. i) * (G . i) ) implies T1 = T2 )
assume that
A5: dom T1 = dom G and
A6: for i being Nat st i in dom T1 holds
T1 . i = (p /. i) * (G . i) and
A7: dom T2 = dom G and
A8: for i being Nat st i in dom T2 holds
T2 . i = (p /. i) * (G . i) ; :: thesis: T1 = T2

now :: thesis: for i being Nat st i in dom G holds
T1 . i = T2 . i

let i be Nat; :: thesis: ( i in dom G implies T1 . i = T2 . i )
assume A9: i in dom G ; :: thesis: T1 . i = T2 . i
thus T1 . i = (p /. i) * (G . i) by A5, A6, A9
.= T2 . i by A7, A8, A9 ; :: thesis: verum

end;

hence T1 = T2 by A5, A7, FINSEQ_1:13; :: thesis: verum