let M1, M2 be Matrix of len b1, len b2,F_Real; :: thesis: ( ( for i, j being Nat st i in dom b1 & j in dom b2 holds
M1 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) & ( for i, j being Nat st i in dom b1 & j in dom b2 holds
M2 * (i,j) = f . ((b1 /. i),(b2 /. j)) ) implies M1 = M2 )
assume that
A22: for i, j being Nat st i in dom b1 & j in dom b2 holds
M1 * (i,j) = f . ((b1 /. i),(b2 /. j)) and
A23: for i, j being Nat st i in dom b1 & j in dom b2 holds
M2 * (i,j) = f . ((b1 /. i),(b2 /. j)) ; :: thesis: M1 = M2

now :: thesis: for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)

let i, j be Nat; :: thesis: ( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )
assume A25: [i,j] in Indices M1 ; :: thesis: M1 * (i,j) = M2 * (i,j)
then len b1 <> 0 by MATRIX_0:22;
then Indices M1 = [:(Seg (len b1)),(Seg (len b2)):] by MATRIX_0:23
.= [:(dom b1),(Seg (len b2)):] by FINSEQ_1:def 3
.= [:(dom b1),(dom b2):] by FINSEQ_1:def 3 ;
then A26: ( i in dom b1 & j in dom b2 ) by A25, ZFMISC_1:87;
thus M1 * (i,j) = f . ((b1 /. i),(b2 /. j)) by A22, A26
.= M2 * (i,j) by A26, A23 ; :: thesis: verum

end;

hence M1 = M2 by MATRIX_0:27; :: thesis: verum