let D be non empty set ; 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; 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; 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; 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; ( 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
; 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;
per cases
( i in dom (Sgm P) or not i in dom (Sgm P) )
;
suppose
i in dom (Sgm P)
;
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)then
(Sgm P) " {((Sgm P) . i)} = {i}
by A8, FINSEQ_5:4;
hence
RLine (
(Segm (A9,P,Q)),
i,
FQ)
= Segm (
(RLine (A9,((Sgm P) . i),F)),
P,
Q)
by A1, A2, A3, A7, A5, Th37;
verum end; suppose A10:
not
i in dom (Sgm P)
;
RLine ((Segm (A9,P,Q)),i,FQ) = Segm ((RLine (A9,((Sgm P) . i),F)),P,Q)A11:
not
0 in Seg (len A9)
;
(Sgm P) . i = 0
by A10, FUNCT_1:def 2;
hence Segm (
(RLine (A9,((Sgm P) . i),F)),
P,
Q) =
Segm (
A9,
P,
Q)
by A11, Th40
.=
RLine (
(Segm (A9,P,Q)),
i,
FQ)
by A9, A4, A10, Th40
;
verum end; end;