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 A66, A69; :: 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 A70, A73; :: 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 (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 :: 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 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; :: thesis: verum

end;

hence F1n . x = F2n . x by A77, A78, A79, A80, FUNCT_1:2; :: thesis: 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; :: thesis: verum

end;

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