let A be Interval; :: thesis: pre-Meas * <*A*> = <*(pre-Meas . A)*>
A1: A in Family_of_Intervals by MEASUR10:def 1;
rng <*A*> = {A} by FINSEQ_1:38;
then reconsider FA = <*A*> as FinSequence of Family_of_Intervals by A1, ZFMISC_1:31, FINSEQ_1:def 4;
( dom pre-Meas = Family_of_Intervals & rng FA c= Family_of_Intervals ) by FUNCT_2:def 1;
then dom (pre-Meas * FA) = dom FA by RELAT_1:27;
then A2: dom (pre-Meas * FA) = Seg 1 by FINSEQ_1:38;
then A3: dom (pre-Meas * FA) = dom <*(pre-Meas . A)*> by FINSEQ_1:38;
for n being Nat st n in dom (pre-Meas * FA) holds
(pre-Meas * FA) . n = <*(pre-Meas . A)*> . n
proof
let n be Nat; :: thesis: ( n in dom (pre-Meas * FA) implies (pre-Meas * FA) . n = <*(pre-Meas . A)*> . n )
assume A4: n in dom (pre-Meas * FA) ; :: thesis: (pre-Meas * FA) . n = <*(pre-Meas . A)*> . n
then A5: n = 1 by A2, FINSEQ_1:2, TARSKI:def 1;
then (pre-Meas * FA) . n = pre-Meas . (FA . 1) by A4, FUNCT_1:12
.= pre-Meas . A by FINSEQ_1:40 ;
hence (pre-Meas * FA) . n = <*(pre-Meas . A)*> . n by A5, FINSEQ_1:40; :: thesis: verum
end;
hence pre-Meas * <*A*> = <*(pre-Meas . A)*> by A3, FINSEQ_1:13; :: thesis: verum