defpred S₁[ set , set , set ] means ( P₁[$1,$2,$3] & $3 in F₁() );
A2: for x, y being set st x in Seg F₂() & y in Seg F₃() holds
ex z being set st
( z in F₁() & S₁[x,y,z] )

proof

let x, y be set ; :: thesis: ( x in Seg F₂() & y in Seg F₃() implies ex z being set st
( z in F₁() & S₁[x,y,z] ) )
assume that
A3: x in Seg F₂() and
A4: y in Seg F₃() ; :: thesis: ex z being set st
( z in F₁() & S₁[x,y,z] )
reconsider y9 = y as Element of NAT by A4;
reconsider x9 = x as Element of NAT by A3;
[x9,y9] in [:(Seg F₂()),(Seg F₃()):] by A3, A4, ZFMISC_1:106;
then consider z9 being Element of F₁() such that
A5: P₁[x9,y9,z9] by A1;
take z9 ; :: thesis: ( z9 in F₁() & S₁[x,y,z9] )
thus ( z9 in F₁() & S₁[x,y,z9] ) by A5; :: thesis: verum

end;

consider f being Function of [:(Seg F₂()),(Seg F₃()):],F₁() such that
A6: for x, y being set st x in Seg F₂() & y in Seg F₃() holds
S₁[x,y,f . x,y] from BINOP_1:sch 1(A2);
A7: F₂() >= 0 by NAT_1:2;
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 ) );
A8: 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) -> set = f . [k,$1];
consider p being FinSequence such that
A9: ( 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 A9, 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 A9; :: thesis: verum

end;

consider M being FinSequence such that
A10: dom M = Seg F₂() and
A11: for k being Nat st k in Seg F₂() holds
S₂[k,M . k] from FINSEQ_1:sch 1(A8);
A12: len M = F₂() by A10, 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
A13: i in Seg F₂() and
A14: M . i = x by A10, FINSEQ_2:11;
consider p being FinSequence such that
A15: M . i = p and
A16: len p = F₃() and
A17: for j being Nat st j in Seg F₃() holds
p . j = f . i,j by A11, 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
A18: k in dom p and
A19: p . k = z by FINSEQ_2:11;
A20: k in Seg (len p) by A18, FINSEQ_1:def 3;
then A21: [i,k] in [:(Seg F₂()),(Seg F₃()):] by A13, A16, ZFMISC_1:106;
z = f . i,k by A16, A17, A19, A20;
hence z in F₁() by A21, FUNCT_2:7; :: thesis: verum

end;

then p is FinSequence of F₁() by FINSEQ_1:def 4;
hence x in F₁() * by A14, A15, 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
A22: i in dom M and
A23: M . i = x by FINSEQ_2:11;
consider p being FinSequence such that
A24: x = p and
A25: len p = F₃() and
A26: for j being Nat st j in Seg F₃() holds
p . j = f . i,j by A10, A11, A22, A23;
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
A27: k in dom p and
A28: p . k = z by FINSEQ_2:11;
A29: k in Seg (len p) by A27, FINSEQ_1:def 3;
then A30: [i,k] in [:(Seg F₂()),(Seg F₃()):] by A10, A22, A25, ZFMISC_1:106;
z = f . i,k by A25, A26, A28, A29;
hence z in F₁() by A30, FUNCT_2:7; :: 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 A24, A25; :: 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
A31: ( i in dom M & M . i = p ) by FINSEQ_2:11;
S₂[i,p] by A10, A11, A31;
hence len p = F₃() ; :: thesis: verum

end;

then reconsider M = M as Matrix of F₂(),F₃(),F₁() by A12, Def3;
take M ; :: thesis: for i, j being Nat st [i,j] in Indices M holds
P₁[i,j,M * i,j]
let i, j be Nat; :: thesis: ( [i,j] in Indices M implies P₁[i,j,M * i,j] )
assume A32: [i,j] in Indices M ; :: thesis: P₁[i,j,M * i,j]
then F₂() <> 0 by A10, ZFMISC_1:106;
then A33: F₂() > 0 by A7, XXREAL_0:1;
j in Seg (width M) by A32, ZFMISC_1:106;
then A34: j in Seg F₃() by A12, A33, Th20;
A35: ex p being FinSequence of F₁() st
( p = M . i & M * i,j = p . j ) by A32, Def6;
A36: i in Seg F₂() by A10, A32, ZFMISC_1:106;
then 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 A11;
then f . i,j = M * i,j by A35, A34;
hence P₁[i,j,M * i,j] by A6, A36, A34; :: thesis: verum