let D be non empty set ; for m, n, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let m, n, m9, n9 be Nat; for A9 being Matrix of n9,m9,D
for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let A9 be Matrix of n9,m9,D; for F, Fmt being FinSequence of D
for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let F, Fmt be FinSequence of D; for nt being Element of n -tuples_on NAT
for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let nt be Element of n -tuples_on NAT; for mt being Element of m -tuples_on NAT st len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 holds
for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let mt be Element of m -tuples_on NAT; ( len F = width A9 & Fmt = F * mt & [:(rng nt),(rng mt):] c= Indices A9 implies for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt) )
assume that
A1:
len F = width A9
and
A2:
Fmt = F * mt
and
A3:
[:(rng nt),(rng mt):] c= Indices A9
; for i, j being Nat st nt " {j} = {i} holds
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
let i, j be Nat; ( nt " {j} = {i} implies RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt) )
assume A4:
nt " {j} = {i}
; RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
A5:
i in {i}
by TARSKI:def 1;
then A6:
i in dom nt
by A4, FUNCT_1:def 7;
then
nt . i in rng nt
by FUNCT_1:def 3;
then
( rng mt = {} or [:(rng nt),(rng mt):] <> {} )
;
then A7:
rng mt c= Seg (width A9)
by A3, ZFMISC_1:114;
nt . i in {j}
by A4, A5, FUNCT_1:def 7;
then A8:
nt . i = j
by TARSKI:def 1;
set R = RLine (A9,j,F);
set SR = Segm ((RLine (A9,j,F)),nt,mt);
set S = Segm (A9,nt,mt);
A9:
dom mt = Seg m
by FINSEQ_2:124;
set RS = RLine ((Segm (A9,nt,mt)),i,Fmt);
A10:
Indices (Segm ((RLine (A9,j,F)),nt,mt)) = Indices (Segm (A9,nt,mt))
by MATRIX_0:26;
dom F = Seg (width A9)
by A1, FINSEQ_1:def 3;
then A11:
dom Fmt = dom mt
by A2, A7, RELAT_1:27;
A12:
width (Segm (A9,nt,mt)) in NAT
by ORDINAL1:def 12;
A13:
n <> 0
by A6;
then
width (Segm (A9,nt,mt)) = m
by MATRIX_0:23;
then A14:
len Fmt = width (Segm (A9,nt,mt))
by A11, A9, FINSEQ_1:def 3, A12;
A15:
Indices A9 = Indices (RLine (A9,j,F))
by MATRIX_0:26;
now for k, l being Nat st [k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt)) holds
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (k,l) = (Segm ((RLine (A9,j,F)),nt,mt)) * (k,l)A16:
dom nt = Seg n
by FINSEQ_2:124;
let k,
l be
Nat;
( [k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt)) implies (RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b1,b2) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b1,b2) )assume A17:
[k,l] in Indices (Segm ((RLine (A9,j,F)),nt,mt))
;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b1,b2) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b1,b2)A18:
Indices (Segm (A9,nt,mt)) = [:(Seg n),(Seg m):]
by A13, MATRIX_0:23;
then A19:
k in Seg n
by A10, A17, ZFMISC_1:87;
reconsider k9 =
k,
l9 =
l as
Element of
NAT by ORDINAL1:def 12;
A20:
(Segm ((RLine (A9,j,F)),nt,mt)) * (
k,
l)
= (RLine (A9,j,F)) * (
(nt . k9),
(mt . l9))
by A17, Def1;
A21:
[(nt . k9),(mt . l9)] in Indices A9
by A3, A15, A17, Th17;
A22:
l in dom mt
by A9, A10, A17, A18, ZFMISC_1:87;
per cases
( k = i or k <> i )
;
suppose A23:
k = i
;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b1,b2) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b1,b2)then A24:
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (
k,
l)
= Fmt . l
by A14, A10, A17, MATRIX11:def 3;
(Segm ((RLine (A9,j,F)),nt,mt)) * (
k,
l)
= F . (mt . l)
by A1, A8, A20, A21, A23, MATRIX11:def 3;
hence
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (
k,
l)
= (Segm ((RLine (A9,j,F)),nt,mt)) * (
k,
l)
by A2, A22, A24, FUNCT_1:13;
verum end; suppose
k <> i
;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (b1,b2) = (Segm ((RLine (A9,j,F)),nt,mt)) * (b1,b2)then
not
k in nt " {j}
by A4, TARSKI:def 1;
then
not
nt . k in {j}
by A19, A16, FUNCT_1:def 7;
then A25:
nt . k <> j
by TARSKI:def 1;
then A26:
(Segm ((RLine (A9,j,F)),nt,mt)) * (
k,
l)
= A9 * (
(nt . k9),
(mt . l9))
by A1, A20, A21, MATRIX11:def 3;
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (
k,
l)
= (Segm (A9,nt,mt)) * (
k,
l)
by A8, A14, A10, A17, A25, MATRIX11:def 3;
hence
(RLine ((Segm (A9,nt,mt)),i,Fmt)) * (
k,
l)
= (Segm ((RLine (A9,j,F)),nt,mt)) * (
k,
l)
by A10, A17, A26, Def1;
verum end; end;
hence
RLine ((Segm (A9,nt,mt)),i,Fmt) = Segm ((RLine (A9,j,F)),nt,mt)
by MATRIX_0:27; verum