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

proof

let x, y be object ; :: thesis: ( x in Seg F₂() & y in Seg F₃() implies ex z being object 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 object st
( z in F₁() & S₁[x,y,z] )
reconsider y9 = y as Nat by A4;
reconsider x9 = x as Nat by A3;
[x9,y9] in [:(Seg F₂()),(Seg F₃()):] by A3, A4, ZFMISC_1:87;
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 object st x in Seg F₂() & y in Seg F₃() holds
S₁[x,y,f . (x,y)] from BINOP_1:sch 1(A2);
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) ) );
A7: 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) -> set = f . [k,$1];
consider p being FinSequence such that
A8: ( 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 A8, 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 A8; :: thesis: verum

end;

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

end;

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

end;

then reconsider M = M as Matrix of F₂(),F₃(),F₁() by A11, Def2;
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 A31: [i,j] in Indices M ; :: thesis: P₁[i,j,M * (i,j)]
then F₂() <> 0 by A9, ZFMISC_1:87;
then A32: F₂() > 0 ;
j in Seg (width M) by A31, ZFMISC_1:87;
then A33: j in Seg F₃() by A11, A32, Th20;
A34: ex p being FinSequence of F₁() st
( p = M . i & M * (i,j) = p . j ) by A31, Def5;
A35: i in Seg F₂() by A9, A31, ZFMISC_1:87;
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 A10;
then f . (i,j) = M * (i,j) by A34, A33;
hence P₁[i,j,M * (i,j)] by A6, A35, A33; :: thesis: verum