let T1, T2 be FinSequence_of_Matrix of K; :: thesis: ( dom T1 = dom G1 & ( for i being Nat st i in dom T1 holds
T1 . i = (G1 . i) * (G2 . i) ) & dom T2 = dom G1 & ( for i being Nat st i in dom T2 holds
T2 . i = (G1 . i) * (G2 . i) ) implies T1 = T2 )
assume that
A5: dom T1 = dom G1 and
A6: for i being Nat st i in dom T1 holds
T1 . i = (G1 . i) * (G2 . i) and
A7: dom T2 = dom G1 and
A8: for i being Nat st i in dom T2 holds
T2 . i = (G1 . i) * (G2 . i) ; :: thesis: T1 = T2
now :: thesis: for i being Nat st i in dom G1 holds
T1 . i = T2 . i
let i be Nat; :: thesis: ( i in dom G1 implies T1 . i = T2 . i )
assume A9: i in dom G1 ; :: thesis: T1 . i = T2 . i
thus T1 . i = (G1 . i) * (G2 . 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