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 )
assume A1: card A = n ; :: thesis: 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 ex A1 being Element of Fin the carrier of C st
( A1 = A & the InternalRel of C linearly_orders A1 ) ;
then ( len (SgmX the InternalRel of C,A) = n & dom (SgmX the InternalRel of C,A) = Seg (len (SgmX the InternalRel of C,A)) ) by A1, Th9, FINSEQ_1:def 3;
hence dom (SgmX the InternalRel of C,A) = Seg n ; :: thesis: verum