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
A2: G = F . f and
A3: ( dom G = the SkeletonSeq of T . (n + 1) & rng G c= the SkeletonSeq of T . n ) by FUNCT_2:def 2;
G . x in rng G by A1, A3, FUNCT_1:def 5;
then reconsider S = G . x as Symplex of T,n by A3;
take S ; :: thesis: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S = G . x
let F1, G1 be Function; :: thesis: ( F1 = the FacesAssign of T . n & G1 = F1 . f implies S = G1 . x )
assume ( F1 = the FacesAssign of T . n & G1 = F1 . f ) ; :: thesis: S = G1 . x
hence S = G1 . x by A2; :: thesis: verum