reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

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

A2: G = F . f and

A3: dom G = the SkeletonSeq of T . (n + 1) and

A4: rng G c= the SkeletonSeq of T . n by FUNCT_2:def 2;

G . x in rng G by A1, A3, FUNCT_1:def 3;

then reconsider S = G . x as Symplex of T,n by A4;

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 that

A5: F1 = the FacesAssign of T . n and

A6: G1 = F1 . f ; :: thesis: S = G1 . x

thus S = G1 . x by A2, A5, A6; :: thesis: verum

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

A2: G = F . f and

A3: dom G = the SkeletonSeq of T . (n + 1) and

A4: rng G c= the SkeletonSeq of T . n by FUNCT_2:def 2;

G . x in rng G by A1, A3, FUNCT_1:def 3;

then reconsider S = G . x as Symplex of T,n by A4;

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 that

A5: F1 = the FacesAssign of T . n and

A6: G1 = F1 . f ; :: thesis: S = G1 . x

thus S = G1 . x by A2, A5, A6; :: thesis: verum