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 A39: F1 . 0 = KX and
A40: F1 . n = P1 and
dom F1 = NAT and
A41: 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 A42: F2 . 0 = KX and
A43: F2 . n = P2 and
dom F2 = NAT and
A44: 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 );
A45: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

A48: S₁[ 0 ] by A39, A42;
for k being Nat holds S₁[k] from NAT_1:sch 2(A48, A45);
hence P1 = P2 by A40, A43; :: thesis: verum