let P1, P2 be SimplicialComplexStr of X; :: thesis: ( ex F being Function st
( F . 0 = KX & F . n = P1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) & ex F being Function st
( F . 0 = KX & F . n = P2 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) implies P1 = P2 )
given F1 being Function such that A40: F1 . 0 = KX and
A41: F1 . n = P1 and
dom F1 = NAT and
A42: for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F1 . k holds
F1 . (k + 1) = subdivision (P,KX1) ; :: thesis: ( for F being Function holds
( not F . 0 = KX or not F . n = P2 or not dom F = NAT or ex k being Nat ex KX1 being SimplicialComplexStr of X st
( KX1 = F . k & not F . (k + 1) = subdivision (P,KX1) ) ) or P1 = P2 )
given F2 being Function such that A43: F2 . 0 = KX and
A44: F2 . n = P2 and
dom F2 = NAT and
A45: for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F2 . k holds
F2 . (k + 1) = subdivision (P,KX1) ; :: thesis: P1 = P2
defpred S₁[ Nat] means ( F1 . $1 = F2 . $1 & ex KX1 being SimplicialComplexStr of X st KX1 = F1 . $1 );
A46: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A47: S₁[k] ; :: thesis: S₁[k + 1]
consider KX1 being SimplicialComplexStr of X such that
A48: KX1 = F1 . k by A47;
F1 . (k + 1) = subdivision (P,KX1) by A42, A48;
hence S₁[k + 1] by A45, A47, A48; :: thesis: verum

end;

A49: S₁[ 0 ] by A40, A43;
for k being Nat holds S₁[k] from NAT_1:sch 2(A49, A46);
hence P1 = P2 by A41, A44; :: thesis: verum