let m, n, k be non zero Nat; :: thesis: for X being non-empty m -element FinSequence
for Y being non-empty n -element FinSequence
for S being sigmaFieldFamily of X st n <= m & Y = X | n holds
SubFin (S,n) is sigmaFieldFamily of Y
let X be non-empty m -element FinSequence; :: thesis: for Y being non-empty n -element FinSequence
for S being sigmaFieldFamily of X st n <= m & Y = X | n holds
SubFin (S,n) is sigmaFieldFamily of Y
let Y be non-empty n -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st n <= m & Y = X | n holds
SubFin (S,n) is sigmaFieldFamily of Y
let S be sigmaFieldFamily of X; :: thesis: ( n <= m & Y = X | n implies SubFin (S,n) is sigmaFieldFamily of Y )
assume that
A1: n <= m and
A2: Y = X | n ; :: thesis: SubFin (S,n) is sigmaFieldFamily of Y
for i being Nat st i in Seg n holds
(SubFin (S,n)) . i is SigmaField of (Y . i)

proof

let i be Nat; :: thesis: ( i in Seg n implies (SubFin (S,n)) . i is SigmaField of (Y . i) )
assume A3: i in Seg n ; :: thesis: (SubFin (S,n)) . i is SigmaField of (Y . i)
A4: Seg n c= Seg m by A1, FINSEQ_1:5;
(S | n) . i = S . i by A3, FUNCT_1:49;
then A5: (S | n) . i is SigmaField of (X . i) by A3, A4, Def2;
Y . i = X . i by A2, A3, FUNCT_1:49;
hence (SubFin (S,n)) . i is SigmaField of (Y . i) by A5, A1, Def6; :: thesis: verum

end;

hence SubFin (S,n) is sigmaFieldFamily of Y by Def2; :: thesis: verum