let D be non empty set ; :: thesis: for i being Nat
for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let i be Nat; :: thesis: for A being Matrix of D
for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let A be Matrix of D; :: thesis: for P, Q being finite without_zero Subset of NAT st i in Seg (card P) & Q c= Seg (width A) holds
Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
let P, Q be finite without_zero Subset of NAT; :: thesis: ( i in Seg (card P) & Q c= Seg (width A) implies Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q) )
assume that
A1: i in Seg (card P) and
A2: Q c= Seg (width A) ; :: thesis: Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q)
rng (Sgm Q) = Q by A2, FINSEQ_1:def 13;
hence Line ((Segm (A,P,Q)),i) = (Line (A,((Sgm P) . i))) * (Sgm Q) by A1, A2, Th24; :: thesis: verum