let D be non empty set ; :: thesis: for i, m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for P, Q being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
let i, m9, n9 be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for P, Q being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
let A9 be Matrix of n9,m9,D; :: thesis: for P, Q being finite without_zero Subset of NAT
for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
let P, Q be finite without_zero Subset of NAT; :: thesis: for F, FQ being FinSequence of D st len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 holds
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
let F, FQ be FinSequence of D; :: thesis: ( len F = width A9 & FQ = F * (Sgm Q) & [:P,Q:] c= Indices A9 implies RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q) )
assume that
A1: len F = width A9 and
A2: FQ = F * (Sgm Q) and
A3: [:P,Q:] c= Indices A9 ; :: thesis: RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)
set SQ = Sgm Q;
set SP = Sgm P;
A4: card P = len (Segm (A9,P,Q)) by MATRIX_0:def 2;
ex m being Nat st Q c= Seg m by Th43;
then A5: rng (Sgm Q) = Q by FINSEQ_1:def 13;
A6: ex n being Nat st P c= Seg n by Th43;
then A7: rng (Sgm P) = P by FINSEQ_1:def 13;
A8: Sgm P is one-to-one by A6, FINSEQ_3:92;
A9: dom (Sgm P) = Seg (card P) by A6, FINSEQ_3:40;