deffunc H_{1}( 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_{1}(n)
from PBOOLE:sch 5();

.= {{}} by FUNCOP_1:def 8 ;

Sk is lower_non-empty

defpred S_{1}[ 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_{1}[y,x,i] )

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_{1}[f . x,x,i] ) )
from MSSUBFAM:sch 1(A15);

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 (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: 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 A60, A62, A65, Def7;

hence face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; :: thesis: verum

consider Sk being SetSequence such that

A1: for n being Element of NAT holds Sk . n = H

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 }

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
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 A3, FUNCOP_1:def 8 ;

:: thesis: verum

end;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 A3, FUNCOP_1:def 8 ;

:: thesis: verum

.= {{}} by FUNCOP_1:def 8 ;

Sk is lower_non-empty

proof

then reconsider Sk = Sk as lower_non-empty SetSequence ;
defpred S_{1}[ 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 & S_{1}[m + 1] holds

S_{1}[m]
_{1}[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

S_{1}[m]
from PRE_POLY:sch 1(A12, A5);

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 A13, A14; :: thesis: verum

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

S

proof

assume A12:
S
let m be Element of NAT ; :: thesis: ( m < n & S_{1}[m + 1] implies S_{1}[m] )

assume that

m < n and

A6: not Sk . (m + 1) is empty ; :: thesis: S_{1}[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 A8, A9, CARD_2:41;

end;assume that

m < n and

A6: not Sk . (m + 1) is empty ; :: thesis: S

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
( m = 0 or m <> 0 )
;

end;

suppose A11:
m <> 0
; :: thesis: S_{1}[m]

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_{1}[m]
by A2, A11; :: thesis: verum

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

not Sk . m is empty

A13: for m being Element of NAT st m <= n holds

S

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 A13, A14; :: thesis: verum

defpred S

( $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

proof

consider F being ManySortedFunction of NatEmbSeq , FuncsSeq Sk such that
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 & S_{1}[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 & S_{1}[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 & S_{1}[y,x,i] ) )

assume A16: x in NatEmbSeq . i ; :: thesis: ex y being object st

( y in (FuncsSeq Sk) . i & S_{1}[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 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_{2}[ 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_{2}[s,u]

A25: dom g = Sk . (n + 1) and

A26: for s being object st s in Sk . (n + 1) holds

S_{2}[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: ( g9 in (FuncsSeq Sk) . i & S_{1}[g9,x,i] )

A27: y2 is one-to-one

hence g9 in (FuncsSeq Sk) . i by Def3; :: thesis: S_{1}[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 A58, A57; :: thesis: verum

end;ex y being object st

( y in (FuncsSeq Sk) . i & S

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 & S

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 & S

assume A16: x in NatEmbSeq . i ; :: thesis: ex y being object st

( y in (FuncsSeq Sk) . i & S

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

( f = $1 & $2 = f * y1 );

A22: for s being object st s in Sk . (n + 1) holds

ex u being object st S

proof

consider g being Function such that
let s be object ; :: thesis: ( s in Sk . (n + 1) implies ex u being object st S_{2}[s,u] )

assume s in Sk . (n + 1) ; :: thesis: ex u being object st S_{2}[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: S_{2}[s,u]

take f ; :: thesis: ( f = s & u = f * y1 )

thus ( f = s & u = f * y1 ) by A23, A24; :: thesis: verum

end;assume s in Sk . (n + 1) ; :: thesis: ex u being object st S

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: S

take f ; :: thesis: ( f = s & u = f * y1 )

thus ( f = s & u = f * y1 ) by A23, A24; :: thesis: verum

A25: dom g = Sk . (n + 1) and

A26: for s being object st s in Sk . (n + 1) holds

S

reconsider y2 = y2 as FinSequence of Seg (n + 1) by A20, FINSEQ_1:def 4;

reconsider g9 = g as set ;

take g9 ; :: thesis: ( g9 in (FuncsSeq Sk) . i & S

A27: y2 is one-to-one

proof

rng g c= Sk . n
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 A28, A29;

end;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 A28, A29;

now :: thesis: not a <> b

hence
a = b
; :: thesis: verumassume A31:
a <> b
; :: thesis: contradiction

end;per cases
( a < b or b < a )
by A31, XXREAL_0:1;

end;

proof

then
g9 in Funcs ((Sk . (n + 1)),(Sk . n))
by A25, FUNCT_2:def 2;
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;

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

end;

suppose A36:
n = 0
; :: thesis: z in Sk . n

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: verum

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

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 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 )

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: verum

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

then A56:
z1 = SgmX ( the InternalRel of C,s9)
by A33, A35, PRE_POLY:9;
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 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: verum

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

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: verum

hence g9 in (FuncsSeq Sk) . i by Def3; :: thesis: S

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 A58, A57; :: thesis: verum

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

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 (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: 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 A60, A62, A65, Def7;

hence face (s,x) = (SgmX ( the InternalRel of C,A)) * x by A62, A63, A64, A65; :: thesis: verum