let S1, S2 be Symplex of T,n; :: thesis: ( ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S1 = G . x ) & ( for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S2 = G . x ) implies S1 = S2 )
assume that
A4: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S1 = G . x and
A5: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S2 = G . x ; :: thesis: S1 = S2
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
reconsider F = the FacesAssign of T . n' as Function of (NatEmbSeq . n'),((FuncsSeq the SkeletonSeq of T) . n') by PBOOLE:def 18;
F . f in (FuncsSeq the SkeletonSeq of T) . n' by FUNCT_2:7;
then F . f in Funcs (the SkeletonSeq of T . (n + 1)),(the SkeletonSeq of T . n) by Def5;
then consider G being Function such that
A6: G = F . f and
( dom G = the SkeletonSeq of T . (n + 1) & rng G c= the SkeletonSeq of T . n ) by FUNCT_2:def 2;
( S1 = G . x & S2 = G . x ) by A4, A5, A6;
hence S1 = S2 ; :: thesis: verum