let D be non empty set ; :: thesis: for n', m' being Nat
for A' being Matrix of n',m',D
for Q being finite without_zero Subset of
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let n', m' be Nat; :: thesis: for A' being Matrix of n',m',D
for Q being finite without_zero Subset of
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let A' be Matrix of n',m',D; :: thesis: for Q being finite without_zero Subset of
for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let Q be finite without_zero Subset of ; :: thesis: for F being FinSequence of D
for i being Nat
for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let F be FinSequence of D; :: thesis: for i being Nat
for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let i be Nat; :: thesis: for P being finite without_zero Subset of st not i in P & [:P,Q:] c= Indices A' holds
Segm A',P,Q = Segm (RLine A',i,F),P,Q
let P be finite without_zero Subset of ; :: thesis: ( not i in P & [:P,Q:] c= Indices A' implies Segm A',P,Q = Segm (RLine A',i,F),P,Q )
assume that
A1: not i in P and
A2: [:P,Q:] c= Indices A' ; :: thesis: Segm A',P,Q = Segm (RLine A',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 A',P,Q = Segm (RLine A',i,F),P,Q by A1, A2, A3, Th38; :: thesis: verum