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