let X be set ; :: thesis: for KX being SimplicialComplexStr of X
for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let KX be SimplicialComplexStr of X; :: thesis: for P being Function
for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let P be Function; :: thesis: for n, k being Element of NAT holds subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
let n, k be Element of NAT ; :: thesis: subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX)))
consider Fn being Function such that
A1: Fn . 0 = subdivision (k,P,KX) and
A2: Fn . n = subdivision (n,P,(subdivision (k,P,KX))) and
dom Fn = NAT and
A3: for m being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fn . m holds
Fn . (m + 1) = subdivision (P,KX1) by Def21;
consider Fnm being Function such that
A4: Fnm . 0 = KX and
A5: Fnm . (n + k) = subdivision ((n + k),P,KX) and
dom Fnm = NAT and
A6: for m being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fnm . m holds
Fnm . (m + 1) = subdivision (P,KX1) by Def21;
defpred S1[ Nat] means ( $1 <= n implies ( Fn . $1 = Fnm . ($1 + k) & ex SX being SimplicialComplexStr of X st Fn . $1 = SX ) );
A7: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A8: S1[m] ; :: thesis: S1[m + 1]
assume A9: m + 1 <= n ; :: thesis: ( Fn . (m + 1) = Fnm . ((m + 1) + k) & ex SX being SimplicialComplexStr of X st Fn . (m + 1) = SX )
then consider SX being SimplicialComplexStr of X such that
A10: Fn . m = SX by A8, NAT_1:13;
subdivision (P,SX) = Fnm . ((m + k) + 1) by A6, A8, A9, A10, NAT_1:13;
hence ( Fn . (m + 1) = Fnm . ((m + 1) + k) & ex SX being SimplicialComplexStr of X st Fn . (m + 1) = SX ) by A3, A10; :: thesis: verum
end;
consider Fm being Function such that
A11: Fm . 0 = KX and
A12: Fm . k = subdivision (k,P,KX) and
dom Fm = NAT and
A13: for m being Nat
for KX1 being SimplicialComplexStr of X st KX1 = Fm . m holds
Fm . (m + 1) = subdivision (P,KX1) by Def21;
defpred S2[ Nat] means ( $1 <= k implies ( Fm . $1 = Fnm . $1 & ex SX being SimplicialComplexStr of X st Fm . $1 = SX ) );
A14: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A15: S2[m] ; :: thesis: S2[m + 1]
assume A16: m + 1 <= k ; :: thesis: ( Fm . (m + 1) = Fnm . (m + 1) & ex SX being SimplicialComplexStr of X st Fm . (m + 1) = SX )
then consider SX being SimplicialComplexStr of X such that
A17: Fm . m = SX by A15, NAT_1:13;
subdivision (P,SX) = Fnm . (m + 1) by A6, A15, A16, A17, NAT_1:13;
hence ( Fm . (m + 1) = Fnm . (m + 1) & ex SX being SimplicialComplexStr of X st Fm . (m + 1) = SX ) by A13, A17; :: thesis: verum
end;
A18: S2[ 0 ] by A4, A11;
for k being Nat holds S2[k] from NAT_1:sch 2(A18, A14);
 then A19: S1[ 0 ] by A1, A12;
for k being Nat holds S1[k] from NAT_1:sch 2(A19, A7);
 hence subdivision ((n + k),P,KX) = subdivision (n,P,(subdivision (k,P,KX))) by A2, A5; :: thesis: verum