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
A58: the SkeletonSeq of T1 . 0 = {{} } and
A59: 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
A60: 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
A61: the SkeletonSeq of T2 . 0 = {{} } and
A62: 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
A63: 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
A64: for x being set st x in NAT holds
the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x

proof

let x be set ; :: 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

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 A58, A61; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n

then A65: n > 0 ;
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 A59;
hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A62, A65; :: thesis: verum

end;

end;

end;

hence the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x ; :: thesis: verum

end;

then A66: the SkeletonSeq of T1 = the SkeletonSeq of T2 by PBOOLE:3;

now

let i be set ; :: 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 (NatEmbSeq . n),((FuncsSeq the SkeletonSeq of T1) . n) by A66, PBOOLE:def 18;
A67: ( dom F1n = NatEmbSeq . n & dom F2n = NatEmbSeq . n ) by FUNCT_2:def 1;

now

let x be set ; :: 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 & F2n . x1 in (FuncsSeq the SkeletonSeq of T1) . n ) ;
then A68: ( F1n . x1 in Funcs (the SkeletonSeq of T1 . (n + 1)),(the SkeletonSeq of T1 . n) & F2n . x1 in Funcs (the SkeletonSeq of T1 . (n + 1)),(the SkeletonSeq of T1 . n) ) by Def5;
then consider F1nx being Function such that
A69: ( F1nx = F1n . x1 & dom F1nx = the SkeletonSeq of T1 . (n + 1) & rng F1nx c= the SkeletonSeq of T1 . n ) by FUNCT_2:def 2;
consider F2nx being Function such that
A70: ( F2nx = F2n . x1 & dom F2nx = the SkeletonSeq of T1 . (n + 1) & rng F2nx c= the SkeletonSeq of T1 . n ) by A68, FUNCT_2:def 2;

now

let y be set ; :: thesis: ( y in the SkeletonSeq of T1 . (n + 1) implies F1nx . y = F2nx . y )
assume A71: y in the SkeletonSeq of T1 . (n + 1) ; :: thesis: F1nx . y = F2nx . y
then reconsider y1 = y as Symplex of T1,(n + 1) ;
reconsider y2 = y as Symplex of T2,(n + 1) by A64, A71;
A72: ( F1nx . y1 = face y1,x1 & F2nx . y2 = face y2,x1 ) by A66, A69, A70, A71, Def10;
y1 in { (SgmX the InternalRel of C,s) where s is non empty Element of symplexes C : card s = n + 1 } by A59, A71;
then consider A being non empty Element of symplexes C such that
A73: ( SgmX the InternalRel of C,A = y1 & card A = n + 1 ) ;
( face y1,x1 = (SgmX the InternalRel of C,A) * x1 & face y2,x1 = (SgmX the InternalRel of C,A) * x1 ) by A60, A63, A66, A71, A73;
hence F1nx . y = F2nx . y by A72; :: thesis: verum

end;

hence F1n . x = F2n . x by A69, A70, FUNCT_1:9; :: thesis: verum

end;

hence the FacesAssign of T1 . i = the FacesAssign of T2 . i by A67, FUNCT_1:9; :: thesis: verum

end;

hence T1 = T2 by A66, PBOOLE:3; :: thesis: verum