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 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 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 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 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 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 A' holds
Segm A',P,Q = Segm (RLine A',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 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 NAT 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 NAT 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 NAT ; :: 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
consider n being Nat such that
A3: P c= Seg n by Th43;
consider m being Nat such that
A4: Q c= Seg m by Th43;
( rng (Sgm P) = P & rng (Sgm Q) = Q ) by A3, A4, FINSEQ_1:def 13;
hence Segm A',P,Q = Segm (RLine A',i,F),P,Q by A1, A2, Th38; :: thesis: verum