let D be non empty set ; :: thesis: for m9, n9 being Nat
for A9 being Matrix of n9,m9,D
for Q being finite without_zero Subset of NAT
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let m9, n9 be Nat; :: thesis: for A9 being Matrix of n9,m9,D
for Q being finite without_zero Subset of NAT
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let A9 be Matrix of n9,m9,D; :: thesis: for Q being finite without_zero Subset of NAT
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let Q be finite without_zero Subset of NAT; :: thesis: for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let F be FinSequence of D; :: thesis: for i being Nat
for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let i be Nat; :: thesis: for P being finite without_zero Subset of NAT st not i in P & [:P,Q:] c= Indices A9 holds
Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
let P be finite without_zero Subset of NAT; :: thesis: ( not i in P & [:P,Q:] c= Indices A9 implies Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q) )
assume that
A1: not i in P and
A2: [:P,Q:] c= Indices A9 ; :: thesis: Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q)
( rng (Sgm Q) = Q & rng (Sgm P) = P ) by FINSEQ_1:def 14;
hence Segm (A9,P,Q) = Segm ((RLine (A9,i,F)),P,Q) by A1, A2, Th38; :: thesis: verum