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 :: thesis: for i being Nat st i in dom f holds
T1 . i = T2 . i

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:13; :: thesis: verum