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
ElmFin (S,k) = ElmFin ((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
ElmFin (S,k) = ElmFin ((SubFin (S,n)),k)
let S be sigmaFieldFamily of X; :: thesis: ( k <= n & n <= m implies ElmFin (S,k) = ElmFin ((SubFin (S,n)),k) )
assume that
A1: k <= n and
A2: n <= m ; :: thesis: ElmFin (S,k) = ElmFin ((SubFin (S,n)),k)
A3: ElmFin (S,k) = S . k by A1, A2, Def7, XXREAL_0:2;
1 <= k by NAT_1:14;
then A4: k in Seg n by A1;
SubFin (S,n) = S | n by A2, Def6;
then ElmFin ((SubFin (S,n)),k) = (S | n) . k by A1, Def7;
hence ElmFin (S,k) = ElmFin ((SubFin (S,n)),k) by A3, A4, FUNCT_1:49; :: thesis: verum