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();
A2: 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 ;

A3: now

let n be Nat; :: thesis:
assume A4: n <> 0 ; :: thesis:
n in NAT by ORDINAL1:def 13;
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 A4, FUNCOP_1:def 8 ;
:: thesis:

end;

Sk is lower_non-empty

proof

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

proof

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

per cases ;

suppose m = 0 ; :: thesis:

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

end;

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

then reconsider sx = sx as non empty Element of symplexes C by A10, Th7, 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 A3, A11; :: thesis:

end;

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

end;

then reconsider Sk = Sk as lower_non-empty SetSequence ;
defpred S₁[ set , set , set ] 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 ) );
A14: for i being set st i in NAT holds
for x being set st x in NatEmbSeq . i holds
ex y being set st
( y in (FuncsSeq Sk) . i & S₁[y,x,i] )

proof

let i be set ; :: thesis:
assume i in NAT ; :: thesis:
then reconsider n = i as Element of NAT ;
let x be set ; :: thesis:
assume A15: x in NatEmbSeq . i ; :: thesis:
then x in { f where f is Element of Funcs (Seg n),(Seg (n + 1)) : @ f is increasing } by Def7;
then consider f being Element of Funcs (Seg n),(Seg (n + 1)) such that
A16: ( f = x & @ f is increasing ) ;
reconsider y = x as Face of n by A15;
reconsider y1 = y as Function ;
consider y2 being Function such that
A17: ( y2 = y1 & dom y2 = Seg n & rng y2 c= Seg (n + 1) ) by A16, FUNCT_2:def 2;
reconsider y2 = y2 as FinSequence by A17, FINSEQ_1:def 2;
A18: len y2 = n by A17, FINSEQ_1:def 3;
reconsider y2 = y2 as FinSequence of Seg (n + 1) by A17, FINSEQ_1:def 4;
A19: y2 is one-to-one

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: thesis:
assume A20: ( a in dom y2 & b in dom y2 & y2 . a = y2 . b ) ; :: thesis:
then reconsider a = a, b = b as Element of NAT ;

now

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

per cases by A21, XXREAL_0:1;

suppose a < b ; :: thesis:

hence contradiction by A16, A17, A20, SEQM_3:def 1; :: thesis:

end;

suppose b < a ; :: thesis:

hence contradiction by A16, A17, A20, SEQM_3:def 1; :: thesis:

end;

hence a = b ; :: thesis:

end;

defpred S₂[ set , set ] means ex f being Function st
( f = $1 & $2 = f * y1 );
A22: for s being set st s in Sk . (n + 1) holds
ex u being set st S₂[s,u]

proof

let s be set ; :: thesis:
assume s in Sk . (n + 1) ; :: thesis:
then s in { (SgmX the InternalRel of C,s') where s' is non empty Element of symplexes C : card s' = n + 1 } by A3;
then consider A being non empty Element of symplexes C such that
A23: ( SgmX the InternalRel of C,A = s & 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 set st s in Sk . (n + 1) holds
S₂[s,g . s] from CLASSES1:sch 1(A22);
reconsider g' = g as set ;
take g' ; :: thesis:
rng g c= Sk . n

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume z in rng g ; :: thesis:
then consider a being set such that
A27: ( a in dom g & z = g . a ) by FUNCT_1:def 5;
consider f being Function such that
A28: ( f = a & g . a = f * y2 ) by A17, A25, A26, A27;
reconsider F = symplexes C as with_non-empty_element Subset of (Fin the carrier of C) ;

per cases ;

suppose A29: n = 0 ; :: thesis:

then dom (f * y1) = {} by A17, FINSEQ_1:4, RELAT_1:44, XBOOLE_1:3;
then z = {} by A17, A27, A28;
hence z in Sk . n by A2, A29, TARSKI:def 1; :: thesis:

end;

suppose A30: 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 A3, A25, A27, A28;
then consider s1 being non empty Element of symplexes C such that
A31: ( SgmX the InternalRel of C,s1 = f & 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 consider s1' being Element of Fin the carrier of C such that
A32: ( s1' = s1 & the InternalRel of C linearly_orders s1' ) ;
rng f = s1 by A31, A32, Def2;
then reconsider f = f as FinSequence of s1 by A31, FINSEQ_1:def 4;
reconsider f = f as FinSequence of RelStr(# s1,(the InternalRel of C |_2 s1) #) ;
A33: f is one-to-one by A31, A32, Th8;
A34: dom f = Seg (n + 1) by A31, Th10;
A35: f is Function of (dom f),s1 by FINSEQ_2:30;
A36: rng f c= s1 by RELAT_1:def 19;
f is Function of (Seg (n + 1)),the carrier of C by A34, A35, FUNCT_2:9;
then reconsider z1 = z as FinSequence of RelStr(# the carrier of C,the InternalRel of C #) by A27, A28, FINSEQ_2:36;
reconsider f = f as Function of (Seg (n + 1)),the carrier of C by A34, A35, FUNCT_2:9;
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;
A37: n in Seg n by A30, FINSEQ_1:5;
A38: dom (f * y2) = Seg n by A17, A34, RELAT_1:46;
for u being set st u in rng (f * y2) holds
u in rng f by FUNCT_1:25;
then rng (f * y2) c= rng f by TARSKI:def 3;
then rng (f * y2) c= s1 by A36, XBOOLE_1:1;
then reconsider s' = r as non empty Element of F by A37, A38, Th7, RELAT_1:65;
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 A39: ( n1 in dom z1 & m1 in dom z1 & n1 < m1 ) ; :: thesis:
then A40: ( z1 . n1 = f . (y2 . n1) & z1 . m1 = f . (y2 . m1) ) by A27, A28, FUNCT_1:22;
y2 . n1 in Seg (n + 1) by A17, A27, A28, A38, A39, FINSEQ_2:13;
then reconsider yn = y2 . n1 as Element of NAT ;
y2 . m1 in Seg (n + 1) by A17, A27, A28, A38, A39, FINSEQ_2:13;
then reconsider ym = y2 . m1 as Element of NAT ;
A41: yn < ym by A16, A17, A27, A28, A38, A39, SEQM_3:def 1;
A42: ( yn in rng y2 & ym in rng y2 ) by A17, A27, A28, A38, A39, FUNCT_1:def 5;
then reconsider fn = f . yn as Element of RelStr(# s1,(the InternalRel of C |_2 s1) #) by A17, A34, FINSEQ_2:13;
reconsider fm = f . ym as Element of RelStr(# s1,(the InternalRel of C |_2 s1) #) by A17, A34, A42, FINSEQ_2:13;
z1 . n1 = fn by A27, A28, A39, FUNCT_1:22;
then reconsider zn = z1 . n1 as Element of RelStr(# s1,(the InternalRel of C |_2 s1) #) ;
z1 . m1 = fm by A27, A28, A39, FUNCT_1:22;
then reconsider zm = z1 . m1 as Element of RelStr(# s1,(the InternalRel of C |_2 s1) #) ;
A43: ( fn = f /. yn & fm = f /. ym ) by A17, A34, A42, PARTFUN1:def 8;
A44: ( zn = z1 /. n1 & zm = z1 /. m1 ) by A39, PARTFUN1:def 8;
set R = the InternalRel of C;
A45: f /. yn = f . yn by A17, A34, A42, PARTFUN1:def 8
.= (SgmX the InternalRel of C,s1) /. yn by A17, A31, A34, A42, PARTFUN1:def 8 ;
f /. ym = f . ym by A17, A34, A42, PARTFUN1:def 8
.= (SgmX the InternalRel of C,s1) /. ym by A17, A31, A34, A42, PARTFUN1:def 8 ;
hence ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) by A17, A31, A32, A34, A40, A41, A42, A43, A44, A45, Def2; :: thesis:

end;

then A46: z1 = SgmX the InternalRel of C,s' by A27, A28, Th4;
A47: f * y2 is one-to-one by A19, A33, FUNCT_1:46;
len (f * y2) = n by A17, A18, A34, FINSEQ_2:33;
then card s' = n by A47, FINSEQ_4:77;
then z in { (SgmX the InternalRel of C,s) where s is non empty Element of symplexes C : card s = n } by A46;
hence z in Sk . n by A3, A30; :: thesis:

end;

then g' in Funcs (Sk . (n + 1)),(Sk . n) by A25, FUNCT_2:def 2;
hence g' in (FuncsSeq Sk) . i by Def5; :: thesis:
take n ; :: thesis:
reconsider y = x as Face of n by A15;
take y ; :: thesis:
thus ( x = y & i = n ) ; :: thesis:
let s be Element of Sk . (n + 1); :: thesis:
assume A48: s in Sk . (n + 1) ; :: thesis:
let A be non empty Element of symplexes C; :: thesis:
assume A49: SgmX the InternalRel of C,A = s ; :: thesis:
consider f being Function such that
A50: ( f = s & g . s = f * y1 ) by A26, A48;
let g1 be Function; :: thesis:
assume g1 = g' ; :: thesis:
hence g1 . s = (SgmX the InternalRel of C,A) * y by A49, A50; :: thesis:

end;

consider F being ManySortedFunction of NatEmbSeq , FuncsSeq Sk such that
A51: for i being set st i in NAT holds
ex f being Function of (NatEmbSeq . i),((FuncsSeq Sk) . i) st
( f = F . i & ( for x being set st x in NatEmbSeq . i holds
S₁[f . x,x,i] ) ) from MSSUBFAM:sch 1(A14);
take TriangStr(# Sk,F #) ; :: thesis:
thus the SkeletonSeq of TriangStr(# Sk,F #) . 0 = {{} } by A2; :: 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 A3; :: thesis:
let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
then consider f1 being Function of (NatEmbSeq . n),((FuncsSeq Sk) . n) such that
A52: f1 = F . n and
A53: for x being set 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 A51;
let x be Face of n; :: thesis:
let s be Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1); :: thesis:
assume A54: s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) ; :: thesis:
let A be non empty Element of symplexes C; :: thesis:
assume A55: SgmX the InternalRel of C,A = s ; :: thesis:
consider m being Nat, y being Face of m such that
A56: ( 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 A53;
f1 . x in (FuncsSeq Sk) . n ;
then f1 . x in Funcs (Sk . (n + 1)),(Sk . n) by Def5;
then consider G being Function such that
A57: f1 . x = G and
( dom G = Sk . (n + 1) & rng G c= Sk . n ) by FUNCT_2:def 2;
face s,x = G . s by A52, A54, A57, Def10;
hence face s,x = (SgmX the InternalRel of C,A) * x by A54, A55, A56, A57; :: thesis: