let n, i be non zero Nat; :: thesis: for X being non-empty n + 1 -element FinSequence
for S being sigmaFieldFamily of X st i <= n holds
CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i))
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being sigmaFieldFamily of X st i <= n holds
CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i))
let S be sigmaFieldFamily of X; :: thesis: ( i <= n implies CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i)) )
assume A1: i <= n ; :: thesis: CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i))
n <= n + 1 by NAT_1:13;
hence CarProduct (SubFin (X,i)) = CarProduct (SubFin ((SubFin (X,n)),i)) by A1, Th7; :: thesis: verum