let D be non empty set ; :: thesis: for n9, m9 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 n9, m9 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
ex m being Nat st Q c= Seg m by Th43;
then A3: rng (Sgm Q) = Q by FINSEQ_1:def 13;
ex n being Nat st P c= Seg n by Th43;
then rng (Sgm P) = P by FINSEQ_1:def 13;
hence Segm A9,P,Q = Segm (RLine A9,i,F),P,Q by A1, A2, A3, Th38; :: thesis: verum