reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
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
A7: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S1 = G . x and
A8: for F, G being Function st F = the FacesAssign of T . n & G = F . f holds
S2 = G . x ; :: thesis: S1 = S2
reconsider F = the FacesAssign of T . n9 as Function of (NatEmbSeq . n9),((FuncsSeq the SkeletonSeq of T) . n9) by PBOOLE:def 15;
F . f in (FuncsSeq the SkeletonSeq of T) . n9 by FUNCT_2:5;
then F . f in Funcs (( the SkeletonSeq of T . (n + 1)),( the SkeletonSeq of T . n)) by Def3;
then consider G being Function such that
A9: G = F . f and
dom G = the SkeletonSeq of T . (n + 1) and
rng G c= the SkeletonSeq of T . n by FUNCT_2:def 2;
S1 = G . x by A7, A9;
hence S1 = S2 by A8, A9; :: thesis: verum