deffunc H₁( Element of NAT ) -> set = IFEQ ($1,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = $1 } );
consider Sk being SetSequence such that
A1: for n being Element of NAT holds Sk . n = H₁(n) from PBOOLE:sch 5();

let n be Nat; :: thesis:
assume A3: n <> 0 ; :: thesis:
n in NAT by ORDINAL1:def 12;
hence Sk . n = IFEQ (n,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } ) by A1
.= { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A3, FUNCOP_1:def 8 ;
:: thesis:

end;

A4: Sk . 0 = IFEQ (0,0,{{}}, { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = 0 } ) by A1
.= {{}} by FUNCOP_1:def 8 ;
Sk is lower_non-empty

proof

defpred S₁[ Nat] means not Sk . $1 is empty ;
let n be Nat; :: according to TRIANG_1:def 2 :: thesis:
A5: for m being Element of NAT st m < n & S₁[m + 1] holds
S₁[m]

proof

let m be Element of NAT ; :: thesis:
assume that
m < n and
A6: not Sk . (m + 1) is empty ; :: thesis:
consider g being object such that
A7: g in Sk . (m + 1) by A6;
Sk . (m + 1) = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = m + 1 } by A2;
then consider s being non empty Element of symplexes C such that
g = SgmX ( the InternalRel of C,s) and
A8: card s = m + 1 by A7;
set x = the Element of s;
reconsider sx = s \ { the Element of s} as finite set ;
sx \/ { the Element of s} = s \/ { the Element of s} by XBOOLE_1:39;
then A9: sx \/ { the Element of s} = s by XBOOLE_1:12;
not the Element of s in sx by ZFMISC_1:56;
then A10: m + 1 = (card sx) + 1 by A8, A9, CARD_2:41;

per cases ;

suppose m = 0 ; :: thesis:

hence S₁[m] by A4; :: thesis:

end;

suppose A11: m <> 0 ; :: thesis:

then reconsider sx = sx as non empty Element of symplexes C by A10, Th5, XBOOLE_1:36;
SgmX ( the InternalRel of C,sx) in { (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = m } by A10;
hence S₁[m] by A2, A11; :: thesis:

end;

assume A12: S₁[n] ; :: thesis:
A13: for m being Element of NAT st m <= n holds
S₁[m] from PRE_POLY:sch 1(A12, A5);
let m be Nat; :: thesis:
assume A14: m < n ; :: thesis:
m in NAT by ORDINAL1:def 12;
hence not Sk . m is empty by A13, A14; :: thesis:

end;

then reconsider Sk = Sk as lower_non-empty SetSequence ;
defpred S₁[ object , object , object ] means ex n being Nat ex y being Face of n st
( $2 = y & $3 = n & ( for s being Element of Sk . (n + 1) st s in Sk . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = $1 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) );
A15: for i being object st i in NAT holds
for x being object st x in NatEmbSeq . i holds
ex y being object st
( y in (FuncsSeq Sk) . i & S₁[y,x,i] )

proof

let i be object ; :: thesis:
assume i in NAT ; :: thesis:
then reconsider n = i as Element of NAT ;
let x be object ; :: thesis:
assume A16: x in NatEmbSeq . i ; :: thesis:
then reconsider y = x as Face of n ;
reconsider y1 = y as Function ;
x in { f where f is Element of Funcs ((Seg n),(Seg (n + 1))) : @ f is increasing } by A16, Def5;
then A17: ex f being Element of Funcs ((Seg n),(Seg (n + 1))) st
( f = x & @ f is increasing ) ;
then consider y2 being Function such that
A18: y2 = y1 and
A19: dom y2 = Seg n and
A20: rng y2 c= Seg (n + 1) by FUNCT_2:def 2;
reconsider y2 = y2 as FinSequence by A19, FINSEQ_1:def 2;
A21: len y2 = n by A19, FINSEQ_1:def 3;
defpred S₂[ object , object ] means ex f being Function st
( f = $1 & $2 = f * y1 );
A22: for s being object st s in Sk . (n + 1) holds
ex u being object st S₂[s,u]

proof

let s be object ; :: thesis:
assume s in Sk . (n + 1) ; :: thesis:
then s in { (SgmX ( the InternalRel of C,s9)) where s9 is non empty Element of symplexes C : card s9 = n + 1 } by A2;
then consider A being non empty Element of symplexes C such that
A23: SgmX ( the InternalRel of C,A) = s and
card A = n + 1 ;
reconsider u = (SgmX ( the InternalRel of C,A)) * y as set ;
consider f being Function such that
A24: f = s by A23;
take u ; :: thesis:
take f ; :: thesis:
thus ( f = s & u = f * y1 ) by A23, A24; :: thesis:

end;

consider g being Function such that
A25: dom g = Sk . (n + 1) and
A26: for s being object st s in Sk . (n + 1) holds
S₂[s,g . s] from CLASSES1:sch 1(A22);
reconsider y2 = y2 as FinSequence of Seg (n + 1) by A20, FINSEQ_1:def 4;
reconsider g9 = g as set ;
take g9 ; :: thesis:
A27: y2 is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A28: a in dom y2 and
A29: b in dom y2 and
A30: y2 . a = y2 . b ; :: thesis:
reconsider a = a, b = b as Element of NAT by A28, A29;

now :: thesis:

assume A31: a <> b ; :: thesis:

per cases by A31, XXREAL_0:1;

suppose a < b ; :: thesis:

hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def 1; :: thesis:

end;

suppose b < a ; :: thesis:

hence contradiction by A17, A18, A28, A29, A30, SEQM_3:def 1; :: thesis:

end;

hence a = b ; :: thesis:

end;

rng g c= Sk . n

proof

reconsider F = symplexes C as with_non-empty_element Subset of (Fin the carrier of C) ;
let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider a being object such that
A32: a in dom g and
A33: z = g . a by FUNCT_1:def 3;
consider f being Function such that
A34: f = a and
A35: g . a = f * y2 by A18, A25, A26, A32;

per cases ;

suppose A36: n = 0 ; :: thesis:

then Seg n = {} ;
then dom (f * y1) = {} by A18, A19, RELAT_1:25, XBOOLE_1:3;
then z = {} by A18, A33, A35;
hence z in Sk . n by A4, A36, TARSKI:def 1; :: thesis:

end;

suppose A37: n <> 0 ; :: thesis:

f in { (SgmX ( the InternalRel of C,s1)) where s1 is non empty Element of symplexes C : card s1 = n + 1 } by A2, A25, A32, A34;
then consider s1 being non empty Element of symplexes C such that
A38: SgmX ( the InternalRel of C,s1) = f and
A39: card s1 = n + 1 ;
s1 in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
then A40: ex s19 being Element of Fin the carrier of C st
( s19 = s1 & the InternalRel of C linearly_orders s19 ) ;
then rng f = s1 by A38, PRE_POLY:def 2;
then reconsider f = f as FinSequence of s1 by A38, FINSEQ_1:def 4;
reconsider f = f as FinSequence of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A41: f is one-to-one by A38, A40, PRE_POLY:10;
A42: dom f = Seg (n + 1) by A38, A39, Th6;
A43: f is Function of (dom f),s1 by FINSEQ_2:26;
then f is Function of (Seg (n + 1)), the carrier of C by A42, FUNCT_2:7;
then reconsider z1 = z as FinSequence of RelStr(# the carrier of C, the InternalRel of C #) by A33, A35, FINSEQ_2:32;
reconsider f = f as Function of (Seg (n + 1)), the carrier of C by A42, A43, FUNCT_2:7;
A44: dom (f * y2) = Seg n by A19, A20, A42, RELAT_1:27;
rng (f * y2) c= the carrier of C by FINSEQ_1:def 4;
then reconsider r = rng (f * y2) as Element of Fin the carrier of C by FINSUB_1:def 5;
rng (f * y2) c= s1 by RELAT_1:def 19;
then reconsider s9 = r as non empty Element of F by A37, A44, Th5, RELAT_1:42;
for n1, m1 being Nat st n1 in dom z1 & m1 in dom z1 & n1 < m1 holds
( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C )

proof

let n1, m1 be Nat; :: thesis:
assume that
A45: n1 in dom z1 and
A46: m1 in dom z1 and
A47: n1 < m1 ; :: thesis:
y2 . m1 in Seg (n + 1) by A19, A33, A35, A44, A46, FINSEQ_2:11;
then reconsider ym = y2 . m1 as Element of NAT ;
y2 . n1 in Seg (n + 1) by A19, A33, A35, A44, A45, FINSEQ_2:11;
then reconsider yn = y2 . n1 as Element of NAT ;
A48: yn < ym by A17, A18, A19, A33, A35, A44, A45, A46, A47, SEQM_3:def 1;
A49: ym in rng y2 by A19, A33, A35, A44, A46, FUNCT_1:def 3;
then reconsider fm = f . ym as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11;
A50: fm = f /. ym by A20, A42, A49, PARTFUN1:def 6;
z1 . m1 = fm by A33, A35, A46, FUNCT_1:12;
then reconsider zm = z1 . m1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A51: zm = z1 /. m1 by A46, PARTFUN1:def 6;
A52: z1 . m1 = f . (y2 . m1) by A33, A35, A46, FUNCT_1:12;
A53: z1 . n1 = f . (y2 . n1) by A33, A35, A45, FUNCT_1:12;
A54: yn in rng y2 by A19, A33, A35, A44, A45, FUNCT_1:def 3;
then reconsider fn = f . yn as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by A20, A42, FINSEQ_2:11;
z1 . n1 = fn by A33, A35, A45, FUNCT_1:12;
then reconsider zn = z1 . n1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A55: zn = z1 /. n1 by A45, PARTFUN1:def 6;
fn = f /. yn by A20, A42, A54, PARTFUN1:def 6;
hence ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) by A20, A38, A40, A42, A53, A52, A48, A54, A49, A50, A55, A51, PRE_POLY:def 2; :: thesis:

end;

then A56: z1 = SgmX ( the InternalRel of C,s9) by A33, A35, PRE_POLY:9;
len (f * y2) = n by A20, A21, A42, FINSEQ_2:29;
then card s9 = n by A27, A41, FINSEQ_4:62;
then z in { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A56;
hence z in Sk . n by A2, A37; :: thesis:

end;

then g9 in Funcs ((Sk . (n + 1)),(Sk . n)) by A25, FUNCT_2:def 2;
hence g9 in (FuncsSeq Sk) . i by Def3; :: thesis:
reconsider y = x as Face of n by A16;
take n ; :: thesis:
take y ; :: thesis:
thus ( x = y & i = n ) ; :: thesis:
let s be Element of Sk . (n + 1); :: thesis:
assume s in Sk . (n + 1) ; :: thesis:
then A57: ex f being Function st
( f = s & g . s = f * y1 ) by A26;
let A be non empty Element of symplexes C; :: thesis:
assume A58: SgmX ( the InternalRel of C,A) = s ; :: thesis:
let g1 be Function; :: thesis:
assume g1 = g9 ; :: thesis:
hence g1 . s = (SgmX ( the InternalRel of C,A)) * y by A58, A57; :: thesis:

end;

consider F being ManySortedFunction of NatEmbSeq , FuncsSeq Sk such that
A59: for i being object st i in NAT holds
ex f being Function of (NatEmbSeq . i),((FuncsSeq Sk) . i) st
( f = F . i & ( for x being object st x in NatEmbSeq . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A15);
take TriangStr(# Sk,F #) ; :: thesis:
thus the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{}} by A4; :: thesis:
thus for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } by A2; :: thesis:
let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 12;
then consider f1 being Function of (NatEmbSeq . n),((FuncsSeq Sk) . n) such that
A60: f1 = F . n and
A61: for x being object st x in NatEmbSeq . n holds
ex m being Nat ex y being Face of m st
( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = f1 . x holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A59;
let x be Face of n; :: thesis:
let s be Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1); :: thesis:
assume A62: s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) ; :: thesis:
let A be non empty Element of symplexes C; :: thesis:
assume A63: SgmX ( the InternalRel of C,A) = s ; :: thesis:
A64: ex m being Nat ex y being Face of m st
( x = y & n = m & ( for s being Element of Sk . (m + 1) st s in Sk . (m + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = f1 . x holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) ) by A61;
f1 . x in (FuncsSeq Sk) . n ;
then f1 . x in Funcs ((Sk . (n + 1)),(Sk . n)) by Def3;
then consider G being Function such that
A65: f1 . x = G and
dom G = Sk . (n + 1) and
rng G c= Sk . n by FUNCT_2:def 2;
face (s,x) = G . s by A60, A62, A65, Def7;
hence face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; :: thesis: