defpred S₁[ set , object ] 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: for k being Nat st k in Seg F₂() holds
ex y being object st S₁[k,y]

proof

let k be Nat; :: thesis: ( k in Seg F₂() implies ex y being object st S₁[k,y] )
assume k in Seg F₂() ; :: thesis: ex y being object st S₁[k,y]
deffunc H₁( Nat) -> Element of F₁() = F₄(k,$1);
consider p being FinSequence such that
A2: ( 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 A2, 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 A2; :: thesis: verum

end;

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

proof

let x be object ; :: 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
A6: i in dom M and
A7: M . i = x by FINSEQ_2:10;
consider p being FinSequence such that
A8: M . i = p and
A9: ( len p = F₃() & ( for j being Nat st j in Seg F₃() holds
p . j = F₄(i,j) ) ) by A3, A4, A6;
rng p c= F₁()

proof

let z be object ; :: 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
A10: k in dom p and
A11: p . k = z by FINSEQ_2:10;
k in Seg (len p) by A10, FINSEQ_1:def 3;
then z = F₄(i,k) by A9, A11;
hence z in F₁() ; :: thesis: verum

end;

then p is FinSequence of F₁() by FINSEQ_1:def 4;
hence x in F₁() * by A7, A8, 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 object 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 object st x in rng M holds
ex p being FinSequence of F₁() st
( x = p & len p = F₃() )
let x be object ; :: 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
A12: ( i in dom M & M . i = x ) by FINSEQ_2:10;
consider p being FinSequence such that
A13: x = p and
A14: len p = F₃() and
A15: for j being Nat st j in Seg F₃() holds
p . j = F₄(i,j) by A3, A4, A12;
rng p c= F₁()

proof

let z be object ; :: 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
A16: k in dom p and
A17: p . k = z by FINSEQ_2:10;
k in Seg (len p) by A16, FINSEQ_1:def 3;
then z = F₄(i,k) by A14, A15, A17;
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 A13, A14; :: 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
A18: ( i in dom M & M . i = p ) by FINSEQ_2:10;
S₁[i,p] by A3, A4, A18;
hence len p = F₃() ; :: thesis: verum

end;

then reconsider M = M as Matrix of F₂(),F₃(),F₁() by A5, Def2;
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 A19: [i,j] in Indices M ; :: thesis: M * (i,j) = F₄(i,j)
then F₂() <> 0 by A3, ZFMISC_1:87;
then A20: F₂() > 0 ;
i in Seg F₂() by A3, A19, ZFMISC_1:87;
then A21: 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 A4;
j in Seg (width M) by A19, ZFMISC_1:87;
then A22: j in Seg F₃() by A5, A20, Th20;
ex p being FinSequence of F₁() st
( p = M . i & M * (i,j) = p . j ) by A19, Def5;
hence M * (i,j) = F₄(i,j) by A21, A22; :: thesis: verum