defpred S₁[ set , set ] means ex p being FinSequence st
( $2 = p & len p = F₃() & ( for i being Nat st i in Seg F₃() holds
p . i = F₄($1,i) ) );
A1: F₂() >= 0 by NAT_1:2;
A2: for k being Nat st k in Seg F₂() holds
ex y being set st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg F₂() implies ex y being set st S₁[k,y] )
assume k in Seg F₂() ; :: thesis: ex y being set st S₁[k,y]
deffunc H₁( Nat) -> Element of F₁() = F₄(k,$1);
consider p being FinSequence such that
A3: ( len p = F₃() & ( for i being Nat st i in dom p holds
p . i = H₁(i) ) ) from FINSEQ_1:sch 2();
take p ; :: thesis: S₁[k,p]
take p ; :: thesis: ( p = p & len p = F₃() & ( for i being Nat st i in Seg F₃() holds
p . i = F₄(k,i) ) )
dom p = Seg F₃() by A3, FINSEQ_1:def 3;
hence ( p = p & len p = F₃() & ( for i being Nat st i in Seg F₃() holds
p . i = F₄(k,i) ) ) by A3; :: thesis: verum

end;

consider M being FinSequence such that
A4: dom M = Seg F₂() and
A5: for k being Nat st k in Seg F₂() holds
S₁[k,M . k] from FINSEQ_1:sch 1(A2);
A6: len M = F₂() by A4, FINSEQ_1:def 3;
rng M c= F₁() *

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng M or x in F₁() * )
assume x in rng M ; :: thesis: x in F₁() *
then consider i being Nat such that
A7: i in dom M and
A8: M . i = x by FINSEQ_2:11;
consider p being FinSequence such that
A9: M . i = p and
A10: ( len p = F₃() & ( for j being Nat st j in Seg F₃() holds
p . j = F₄(i,j) ) ) by A4, A5, A7;
rng p c= F₁()

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F₁() )
assume z in rng p ; :: thesis: z in F₁()
then consider k being Nat such that
A11: k in dom p and
A12: p . k = z by FINSEQ_2:11;
k in Seg (len p) by A11, FINSEQ_1:def 3;
then z = F₄(i,k) by A10, A12;
hence z in F₁() ; :: thesis: verum

end;

then p is FinSequence of F₁() by FINSEQ_1:def 4;
hence x in F₁() * by A8, A9, FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider M = M as FinSequence of F₁() * by FINSEQ_1:def 4;
ex n being Nat st
for x being set st x in rng M holds
ex p being FinSequence of F₁() st
( x = p & len p = n )

proof

take F₃() ; :: thesis: for x being set st x in rng M holds
ex p being FinSequence of F₁() st
( x = p & len p = F₃() )
let x be set ; :: thesis: ( x in rng M implies ex p being FinSequence of F₁() st
( x = p & len p = F₃() ) )
assume x in rng M ; :: thesis: ex p being FinSequence of F₁() st
( x = p & len p = F₃() )
then consider i being Nat such that
A13: ( i in dom M & M . i = x ) by FINSEQ_2:11;
consider p being FinSequence such that
A14: x = p and
A15: len p = F₃() and
A16: for j being Nat st j in Seg F₃() holds
p . j = F₄(i,j) by A4, A5, A13;
rng p c= F₁()

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng p or z in F₁() )
assume z in rng p ; :: thesis: z in F₁()
then consider k being Nat such that
A17: k in dom p and
A18: p . k = z by FINSEQ_2:11;
k in Seg (len p) by A17, FINSEQ_1:def 3;
then z = F₄(i,k) by A15, A16, A18;
hence z in F₁() ; :: thesis: verum

end;

then reconsider p = p as FinSequence of F₁() by FINSEQ_1:def 4;
take p ; :: thesis: ( x = p & len p = F₃() )
thus ( x = p & len p = F₃() ) by A14, A15; :: thesis: verum

end;

then reconsider M = M as Matrix of F₁() by Th9;
for p being FinSequence of F₁() st p in rng M holds
len p = F₃()

proof

let p be FinSequence of F₁(); :: thesis: ( p in rng M implies len p = F₃() )
assume p in rng M ; :: thesis: len p = F₃()
then consider i being Nat such that
A19: ( i in dom M & M . i = p ) by FINSEQ_2:11;
S₁[i,p] by A4, A5, A19;
hence len p = F₃() ; :: thesis: verum

end;

then reconsider M = M as Matrix of F₂(),F₃(),F₁() by A6, Def3;
take M ; :: thesis: for i, j being Nat st [i,j] in Indices M holds
M * i,j = F₄(i,j)
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies M * i,j = F₄(i,j) )
assume A20: [i,j] in Indices M ; :: thesis: M * i,j = F₄(i,j)
then F₂() <> 0 by A4, ZFMISC_1:106;
then A21: F₂() > 0 by A1, XXREAL_0:1;
i in Seg F₂() by A4, A20, ZFMISC_1:106;
then A22: ex q being FinSequence st
( M . i = q & len q = F₃() & ( for j being Nat st j in Seg F₃() holds
q . j = F₄(i,j) ) ) by A5;
j in Seg (width M) by A20, ZFMISC_1:106;
then A23: j in Seg F₃() by A6, A21, Th20;
ex p being FinSequence of F₁() st
( p = M . i & M * i,j = p . j ) by A20, Def6;
hence M * i,j = F₄(i,j) by A22, A23; :: thesis: verum