deffunc H1( 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 = H1(n) from PBOOLE:sch 5();
A2: now :: thesis: for n being Nat st n <> 0 holds
Sk . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n }
let n be Nat; :: thesis: ( n <> 0 implies Sk . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n } )
assume A3: n <> 0 ; :: thesis: Sk . n = { (SgmX ( the InternalRel of C,s)) where s is non empty Element of symplexes C : card s = n }
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 ;
:: thesis: verum
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 S1[ Nat] means not Sk . \$1 is empty ;
let n be Nat; :: according to TRIANG_1:def 2 :: thesis: ( not Sk . n is empty implies for m being Nat st m < n holds
not Sk . m is empty )

A5: for m being Element of NAT st m < n & S1[m + 1] holds
S1[m]
proof
let m be Element of NAT ; :: thesis: ( m < n & S1[m + 1] implies S1[m] )
assume that
m < n and
A6: not Sk . (m + 1) is empty ; :: thesis: S1[m]
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 ;
per cases ( m = 0 or m <> 0 ) ;
suppose A11: m <> 0 ; :: thesis: S1[m]
then reconsider sx = sx as non empty Element of symplexes C by ;
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 S1[m] by A2, A11; :: thesis: verum
end;
end;
end;
assume A12: S1[n] ; :: thesis: for m being Nat st m < n holds
not Sk . m is empty

A13: for m being Element of NAT st m <= n holds
S1[m] from let m be Nat; :: thesis: ( m < n implies not Sk . m is empty )
assume A14: m < n ; :: thesis: not Sk . m is empty
m in NAT by ORDINAL1:def 12;
hence not Sk . m is empty by ; :: thesis: verum
end;
then reconsider Sk = Sk as lower_non-empty SetSequence ;
defpred S1[ 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 & S1[y,x,i] )
proof
let i be object ; :: thesis: ( i in NAT implies for x being object st x in NatEmbSeq . i holds
ex y being object st
( y in (FuncsSeq Sk) . i & S1[y,x,i] ) )

assume i in NAT ; :: thesis: for x being object st x in NatEmbSeq . i holds
ex y being object st
( y in (FuncsSeq Sk) . i & S1[y,x,i] )

then reconsider n = i as Element of NAT ;
let x be object ; :: thesis: ( x in NatEmbSeq . i implies ex y being object st
( y in (FuncsSeq Sk) . i & S1[y,x,i] ) )

assume A16: x in NatEmbSeq . i ; :: thesis: ex y being object st
( y in (FuncsSeq Sk) . i & S1[y,x,i] )

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 ;
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 ;
A21: len y2 = n by ;
defpred S2[ 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 S2[s,u]
proof
let s be object ; :: thesis: ( s in Sk . (n + 1) implies ex u being object st S2[s,u] )
assume s in Sk . (n + 1) ; :: thesis: ex u being object st S2[s,u]
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: S2[s,u]
take f ; :: thesis: ( f = s & u = f * y1 )
thus ( f = s & u = f * y1 ) by ; :: thesis: verum
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
S2[s,g . s] from reconsider y2 = y2 as FinSequence of Seg (n + 1) by ;
reconsider g9 = g as set ;
take g9 ; :: thesis: ( g9 in (FuncsSeq Sk) . i & S1[g9,x,i] )
A27: y2 is one-to-one
proof
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom y2 or not b in dom y2 or not y2 . a = y2 . b or a = b )
assume that
A28: a in dom y2 and
A29: b in dom y2 and
A30: y2 . a = y2 . b ; :: thesis: a = b
reconsider a = a, b = b as Element of NAT by ;
now :: thesis: not a <> b
assume A31: a <> b ; :: thesis: contradiction
end;
hence a = b ; :: thesis: verum
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: ( not z in rng g or z in Sk . n )
assume z in rng g ; :: thesis: z in Sk . n
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 ( n = 0 or n <> 0 ) ;
suppose A36: n = 0 ; :: thesis: z in Sk . n
then Seg n = {} ;
then dom (f * y1) = {} by ;
then z = {} by ;
hence z in Sk . n by ; :: thesis: verum
end;
suppose A37: n <> 0 ; :: thesis: z in Sk . n
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 ;
then reconsider f = f as FinSequence of s1 by ;
reconsider f = f as FinSequence of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A41: f is one-to-one by ;
A42: dom f = Seg (n + 1) by ;
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 ;
then reconsider z1 = z as FinSequence of RelStr(# the carrier of C, the InternalRel of C #) by ;
reconsider f = f as Function of (Seg (n + 1)), the carrier of C by ;
A44: dom (f * y2) = Seg n by ;
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 ;
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: ( n1 in dom z1 & m1 in dom z1 & n1 < m1 implies ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) )
assume that
A45: n1 in dom z1 and
A46: m1 in dom z1 and
A47: n1 < m1 ; :: thesis: ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C )
y2 . m1 in Seg (n + 1) by ;
then reconsider ym = y2 . m1 as Element of NAT ;
y2 . n1 in Seg (n + 1) by ;
then reconsider yn = y2 . n1 as Element of NAT ;
A48: yn < ym by ;
A49: ym in rng y2 by ;
then reconsider fm = f . ym as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by ;
A50: fm = f /. ym by ;
z1 . m1 = fm by ;
then reconsider zm = z1 . m1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A51: zm = z1 /. m1 by ;
A52: z1 . m1 = f . (y2 . m1) by ;
A53: z1 . n1 = f . (y2 . n1) by ;
A54: yn in rng y2 by ;
then reconsider fn = f . yn as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) by ;
z1 . n1 = fn by ;
then reconsider zn = z1 . n1 as Element of RelStr(# s1,( the InternalRel of C |_2 s1) #) ;
A55: zn = z1 /. n1 by ;
fn = f /. yn by ;
hence ( z1 /. n1 <> z1 /. m1 & [(z1 /. n1),(z1 /. m1)] in the InternalRel of C ) by ; :: thesis: verum
end;
then A56: z1 = SgmX ( the InternalRel of C,s9) by ;
len (f * y2) = n by ;
then card s9 = n by ;
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 ; :: thesis: verum
end;
end;
end;
then g9 in Funcs ((Sk . (n + 1)),(Sk . n)) by ;
hence g9 in (FuncsSeq Sk) . i by Def3; :: thesis: S1[g9,x,i]
reconsider y = x as Face of n by A16;
take n ; :: thesis: ex y being Face of n st
( x = y & i = 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 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) )

take y ; :: thesis: ( x = y & i = 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 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y ) )

thus ( x = y & i = n ) ; :: thesis: 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 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y

let s be Element of Sk . (n + 1); :: thesis: ( s in Sk . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y )

assume s in Sk . (n + 1) ; :: thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y

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: ( SgmX ( the InternalRel of C,A) = s implies for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y )

assume A58: SgmX ( the InternalRel of C,A) = s ; :: thesis: for g1 being Function st g1 = g9 holds
g1 . s = (SgmX ( the InternalRel of C,A)) * y

let g1 be Function; :: thesis: ( g1 = g9 implies g1 . s = (SgmX ( the InternalRel of C,A)) * y )
assume g1 = g9 ; :: thesis: g1 . s = (SgmX ( the InternalRel of C,A)) * y
hence g1 . s = (SgmX ( the InternalRel of C,A)) * y by ; :: thesis: verum
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 (),((FuncsSeq Sk) . i) st
( f = F . i & ( for x being object st x in NatEmbSeq . i holds
S1[f . x,x,i] ) ) from take TriangStr(# Sk,F #) ; :: thesis: ( the SkeletonSeq of TriangStr(# Sk,F #) . 0 = & ( for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . 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 TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (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 ) )

thus the SkeletonSeq of TriangStr(# Sk,F #) . 0 = by A4; :: thesis: ( ( for n being Nat st n > 0 holds
the SkeletonSeq of TriangStr(# Sk,F #) . 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 TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (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 ) )

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: for n being Nat
for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (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

let n be Nat; :: thesis: for f being Face of n
for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (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

n in NAT by ORDINAL1:def 12;
then consider f1 being Function of (),((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: for s being Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) st s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) holds
for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x

let s be Element of the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1); :: thesis: ( s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) implies for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x )

assume A62: s in the SkeletonSeq of TriangStr(# Sk,F #) . (n + 1) ; :: thesis: for A being non empty Element of symplexes C st SgmX ( the InternalRel of C,A) = s holds
face (s,x) = (SgmX ( the InternalRel of C,A)) * x

let A be non empty Element of symplexes C; :: thesis: ( SgmX ( the InternalRel of C,A) = s implies face (s,x) = (SgmX ( the InternalRel of C,A)) * x )
assume A63: SgmX ( the InternalRel of C,A) = s ; :: thesis: face (s,x) = (SgmX ( the InternalRel of C,A)) * x
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 ;
hence face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; :: thesis: verum