A1: ( len X = m & len S = m ) by CARD_1:def 7;
SubFin (X,m) = X | m by Def5;
then A2: SubFin (X,m) = X by A1, FINSEQ_1:58;
A3: SubFin (S,m) = S | m by Def6;
S | m = S by A1, FINSEQ_1:58;
hence (ProdSigmaMesFinSeq M) . m is sigma_Measure of (Prod_Field S) by A2, A3, Th22; :: thesis: verum