let T1, T2 be strict lower_non-empty TriangStr ; :: thesis: ( the SkeletonSeq of T1 . 0 = & ( for n being Nat st n > 0 holds
the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) & the SkeletonSeq of T2 . 0 = & ( for n being Nat st n > 0 holds
the SkeletonSeq of T2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } ) & ( for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ) implies T1 = T2 )

assume that
A66: the SkeletonSeq of T1 . 0 = and
A67: for n being Nat st n > 0 holds
the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } and
A68: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T1 . (n + 1) st s in the SkeletonSeq of T1 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f and
A69: the SkeletonSeq of T2 . 0 = and
A70: for n being Nat st n > 0 holds
the SkeletonSeq of T2 . n = { (SgmX ( the InternalRel of C,A)) where A is non empty Element of symplexes C : card A = n } and
A71: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of T2 . (n + 1) st s in the SkeletonSeq of T2 . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,f) = (SgmX ( the InternalRel of C,A)) * f ; :: thesis: T1 = T2
A72: for x being object st x in NAT holds
the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
proof
let x be object ; :: thesis: ( x in NAT implies the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x )
assume x in NAT ; :: thesis: the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
then reconsider n = x as Element of NAT ;
now :: thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n
hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by ; :: thesis: verum
end;
suppose A73: n <> 0 ; :: thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n
then the SkeletonSeq of T1 . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A67;
hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by ; :: thesis: verum
end;
end;
end;
hence the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x ; :: thesis: verum
end;
then A74: the SkeletonSeq of T1 = the SkeletonSeq of T2 ;
now :: thesis: for i being object st i in NAT holds
the FacesAssign of T1 . i = the FacesAssign of T2 . i
let i be object ; :: thesis: ( i in NAT implies the FacesAssign of T1 . i = the FacesAssign of T2 . i )
assume i in NAT ; :: thesis: the FacesAssign of T1 . i = the FacesAssign of T2 . i
then reconsider n = i as Element of NAT ;
reconsider F1n = the FacesAssign of T1 . n, F2n = the FacesAssign of T2 . n as Function of (),((FuncsSeq the SkeletonSeq of T1) . n) by ;
A75: dom F2n = NatEmbSeq . n by FUNCT_2:def 1;
A76: now :: thesis: for x being object st x in NatEmbSeq . n holds
F1n . x = F2n . x
let x be object ; :: thesis: ( x in NatEmbSeq . n implies F1n . x = F2n . x )
assume x in NatEmbSeq . n ; :: thesis: F1n . x = F2n . x
then reconsider x1 = x as Face of n ;
F1n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ;
then F1n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3;
then consider F1nx being Function such that
A77: F1nx = F1n . x1 and
A78: dom F1nx = the SkeletonSeq of T1 . (n + 1) and
rng F1nx c= the SkeletonSeq of T1 . n by FUNCT_2:def 2;
F2n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ;
then F2n . x1 in Funcs (( the SkeletonSeq of T1 . (n + 1)),( the SkeletonSeq of T1 . n)) by Def3;
then consider F2nx being Function such that
A79: F2nx = F2n . x1 and
A80: dom F2nx = the SkeletonSeq of T1 . (n + 1) and
rng F2nx c= the SkeletonSeq of T1 . n by FUNCT_2:def 2;
now :: thesis: for y being object st y in the SkeletonSeq of T1 . (n + 1) holds
F1nx . y = F2nx . y
let y be object ; :: thesis: ( y in the SkeletonSeq of T1 . (n + 1) implies F1nx . y = F2nx . y )
assume A81: y in the SkeletonSeq of T1 . (n + 1) ; :: thesis: F1nx . y = F2nx . y
then reconsider y1 = y as Symplex of T1,(n + 1) ;
A82: F1nx . y1 = face (y1,x1) by ;
reconsider y2 = y as Symplex of T2,(n + 1) by ;
A83: F2nx . y2 = face (y2,x1) by ;
y1 in { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n + 1 } by ;
then consider A being non empty Element of symplexes C such that
A84: SgmX ( the InternalRel of C,A) = y1 and
card A = n + 1 ;
face (y1,x1) = (SgmX ( the InternalRel of C,A)) * x1 by ;
hence F1nx . y = F2nx . y by A71, A74, A81, A82, A83, A84; :: thesis: verum
end;
hence F1n . x = F2n . x by ; :: thesis: verum
end;
dom F1n = NatEmbSeq . n by FUNCT_2:def 1;
hence the FacesAssign of T1 . i = the FacesAssign of T2 . i by ; :: thesis: verum
end;
hence T1 = T2 by ; :: thesis: verum