let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X st k <= n & n <= m holds
SubFin (S,k) = SubFin ((SubFin (S,n)),k)
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st k <= n & n <= m holds
SubFin (S,k) = SubFin ((SubFin (S,n)),k)
let S be sigmaFieldFamily of X; :: thesis: ( k <= n & n <= m implies SubFin (S,k) = SubFin ((SubFin (S,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: SubFin (S,k) = SubFin ((SubFin (S,n)),k)
SubFin ((SubFin (S,n)),k) = (SubFin (S,n)) | k by A1, Def6;
then SubFin ((SubFin (S,n)),k) = (S | n) | k by A2, Def6;
then SubFin ((SubFin (S,n)),k) = S | k by A1, FINSEQ_1:82;
hence SubFin (S,k) = SubFin ((SubFin (S,n)),k) by A2, A1, Def6, XXREAL_0:2; :: thesis: verum