let m, n be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for S being sigmaFieldFamily of X st n <= m holds
S . n is SigmaField of (ElmFin (X,n))
let X be non-empty m -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st n <= m holds
S . n is SigmaField of (ElmFin (X,n))
let S be sigmaFieldFamily of X; :: thesis: ( n <= m implies S . n is SigmaField of (ElmFin (X,n)) )
assume A1: n <= m ; :: thesis: S . n is SigmaField of (ElmFin (X,n))
then A2: ElmFin (X,n) = X . n by Def1;
1 <= n by NAT_1:14;
then n in Seg m by A1;
hence S . n is SigmaField of (ElmFin (X,n)) by A2, Def2; :: thesis: verum