let n be Element of NAT ; :: thesis: for C being non empty Poset
for A being non empty Element of symplexes C st card A = n holds
dom (SgmX the InternalRel of C,A) = Seg n
let C be non empty Poset; :: thesis: for A being non empty Element of symplexes C st card A = n holds
dom (SgmX the InternalRel of C,A) = Seg n
let A be non empty Element of symplexes C; :: thesis: ( card A = n implies dom (SgmX the InternalRel of C,A) = Seg n )
set f = SgmX the InternalRel of C,A;
A in { A1 where A1 is Element of Fin the carrier of C : the InternalRel of C linearly_orders A1 } ;
then A1: ex A1 being Element of Fin the carrier of C st
( A1 = A & the InternalRel of C linearly_orders A1 ) ;
assume card A = n ; :: thesis: dom (SgmX the InternalRel of C,A) = Seg n
then len (SgmX the InternalRel of C,A) = n by A1, PRE_POLY:11;
hence dom (SgmX the InternalRel of C,A) = Seg n by FINSEQ_1:def 3; :: thesis: verum