let a, b be Real_Sequence; :: thesis: for i being Nat holds (IntervalSequence (a,b)) . i = product <*[.(a . i),(b . i).]*>
let i be Nat; :: thesis: (IntervalSequence (a,b)) . i = product <*[.(a . i),(b . i).]*>
consider f being Function of NAT,(bool (REAL 1)) such that
A1: IntervalSequence (a,b) = f and
A2: for i being Nat holds f . i = product <*[.(a . i),(b . i).]*> by Def1;
thus (IntervalSequence (a,b)) . i = product <*[.(a . i),(b . i).]*> by A1, A2; :: thesis: verum