let T1, T2 be strict lower_non-empty TriangStr ; ( 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
; T1 = T2
A72:
for x being object st x in NAT holds
the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
then A74:
the SkeletonSeq of T1 = the SkeletonSeq of T2
;
now for i being object st i in NAT holds
the FacesAssign of T1 . i = the FacesAssign of T2 . ilet i be
object ;
( i in NAT implies the FacesAssign of T1 . i = the FacesAssign of T2 . i )assume
i in NAT
;
the FacesAssign of T1 . i = the FacesAssign of T2 . ithen 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 A74, PBOOLE:def 15;
A75:
dom F2n = NatEmbSeq . n
by FUNCT_2:def 1;
A76:
now for x being object st x in NatEmbSeq . n holds
F1n . x = F2n . xlet x be
object ;
( x in NatEmbSeq . n implies F1n . x = F2n . x )assume
x in NatEmbSeq . n
;
F1n . x = F2n . xthen 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 for y being object st y in the SkeletonSeq of T1 . (n + 1) holds
F1nx . y = F2nx . ylet y be
object ;
( y in the SkeletonSeq of T1 . (n + 1) implies F1nx . y = F2nx . y )assume A81:
y in the
SkeletonSeq of
T1 . (n + 1)
;
F1nx . y = F2nx . ythen reconsider y1 =
y as
Symplex of
T1,
(n + 1) ;
A82:
F1nx . y1 = face (
y1,
x1)
by A77, A81, Def7;
reconsider y2 =
y as
Symplex of
T2,
(n + 1) by A72, A81;
A83:
F2nx . y2 = face (
y2,
x1)
by A74, A79, A81, Def7;
y1 in { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n + 1 }
by A67, A81;
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 A68, A81, A84;
hence
F1nx . y = F2nx . y
by A71, A74, A81, A82, A83, A84;
verum end; hence
F1n . x = F2n . x
by A77, A78, A79, A80, FUNCT_1:2;
verum end;
dom F1n = NatEmbSeq . n
by FUNCT_2:def 1;
hence
the
FacesAssign of
T1 . i = the
FacesAssign of
T2 . i
by A75, A76, FUNCT_1:2;
verum end;
hence
T1 = T2
by A74, PBOOLE:3; verum