let T1, T2 be FinSequence_of_Square-Matrix of K; :: thesis: ( dom T1 = dom f & ( for i being Nat st i in dom T1 holds
T1 . i = 1. K,(f . i) ) & dom T2 = dom f & ( for i being Nat st i in dom T2 holds
T2 . i = 1. K,(f . i) ) implies T1 = T2 )
assume that
A8: ( dom T1 = dom f & ( for i being Nat st i in dom T1 holds
T1 . i = 1. K,(f . i) ) ) and
A9: ( dom T2 = dom f & ( for i being Nat st i in dom T2 holds
T2 . i = 1. K,(f . i) ) ) ; :: thesis: T1 = T2

now

let i be Nat; :: thesis: ( i in dom f implies T1 . i = T2 . i )
assume A10: i in dom f ; :: thesis: T1 . i = T2 . i
thus T1 . i = 1. K,(f . i) by A8, A10
.= T2 . i by A9, A10 ; :: thesis: verum

end;

hence T1 = T2 by A8, A9, FINSEQ_1:17; :: thesis: verum