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

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