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
A5: dom T1 = dom f and
A6: for i being Nat st i in dom T1 holds
T1 . i = 1. K,(f . i) and
A7: dom T2 = dom f and
A8: 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 A9: i in dom f ; :: thesis: T1 . i = T2 . i
thus T1 . i = 1. K,(f . i) by A5, A6, A9
.= T2 . i by A7, A8, A9 ; :: thesis: verum

end;

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