defpred S1[ set , object ] means ex p being FinSequence st
( $2 = p & len p = F3() & ( for i being Nat st i in Seg F3() holds
p . i = F4($1,i) ) );
A1:
for k being Nat st k in Seg F2() holds
ex y being object st S1[k,y]
consider M being FinSequence such that
A3:
dom M = Seg F2()
and
A4:
for k being Nat st k in Seg F2() holds
S1[k,M . k]
from FINSEQ_1:sch 1(A1);
F2() in NAT
by ORDINAL1:def 12;
then A5:
len M = F2()
by A3, FINSEQ_1:def 3;
rng M c= F1() *
then reconsider M = M as FinSequence of F1() * by FINSEQ_1:def 4;
ex n being Nat st
for x being object st x in rng M holds
ex p being FinSequence of F1() st
( x = p & len p = n )
then reconsider M = M as Matrix of F1() by Th9;
for p being FinSequence of F1() st p in rng M holds
len p = F3()
then reconsider M = M as Matrix of F2(),F3(),F1() by A5, Def2;
take
M
; for i, j being Nat st [i,j] in Indices M holds
M * (i,j) = F4(i,j)
let i, j be Nat; ( [i,j] in Indices M implies M * (i,j) = F4(i,j) )
assume A19:
[i,j] in Indices M
; M * (i,j) = F4(i,j)
then
F2() <> 0
by A3, ZFMISC_1:87;
then A20:
F2() > 0
;
i in Seg F2()
by A3, A19, ZFMISC_1:87;
then A21:
ex q being FinSequence st
( M . i = q & len q = F3() & ( for j being Nat st j in Seg F3() holds
q . j = F4(i,j) ) )
by A4;
j in Seg (width M)
by A19, ZFMISC_1:87;
then A22:
j in Seg F3()
by A5, A20, Th20;
ex p being FinSequence of F1() st
( p = M . i & M * (i,j) = p . j )
by A19, Def5;
hence
M * (i,j) = F4(i,j)
by A21, A22; verum