let M1, M2 be Matrix of len b1, len b2,F_Real; ( ( 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))
; M1 = M2
now for i, j being Nat st [i,j] in Indices M1 holds
M1 * (i,j) = M2 * (i,j)let i,
j be
Nat;
( [i,j] in Indices M1 implies M1 * (i,j) = M2 * (i,j) )assume A25:
[i,j] in Indices M1
;
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
;
verum end;
hence
M1 = M2
by MATRIX_0:27; verum