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

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

then A74:
the SkeletonSeq of T1 = the SkeletonSeq of T2
;
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 ;

end;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 . nend;

hence
the SkeletonSeq of T1 . x = the SkeletonSeq of T2 . x
; :: thesis: verumper cases
( n = 0 or n <> 0 )
;

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;hence the SkeletonSeq of T1 . n = the SkeletonSeq of T2 . n by A70, A73; :: thesis: verum

now :: thesis: for i being object st i in NAT holds

the FacesAssign of T1 . i = the FacesAssign of T2 . i

hence
T1 = T2
by A74, PBOOLE:3; :: thesis: verumthe 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;

hence the FacesAssign of T1 . i = the FacesAssign of T2 . i by A75, A76, FUNCT_1:2; :: thesis: verum

end;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

dom F1n = NatEmbSeq . n
by FUNCT_2:def 1;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;

end;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

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

hence the FacesAssign of T1 . i = the FacesAssign of T2 . i by A75, A76, FUNCT_1:2; :: thesis: verum