let f1, f2 be real-valued FinSequence; :: thesis: for r being Real holds (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
let r be Real; :: thesis: (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r)
set I1 = Intervals (f1,r);
set I2 = Intervals (f2,r);
set f12 = f1 ^ f2;
set I12 = Intervals ((f1 ^ f2),r);
A1: dom (Intervals ((f1 ^ f2),r)) = dom (f1 ^ f2) by EUCLID_9:def 3;
A2: ( len (f1 ^ f2) = (len f1) + (len f2) & len ((Intervals (f1,r)) ^ (Intervals (f2,r))) = (len (Intervals (f1,r))) + (len (Intervals (f2,r))) ) by FINSEQ_1:22;
A3: dom (Intervals (f1,r)) = dom f1 by EUCLID_9:def 3;
then A4: len (Intervals (f1,r)) = len f1 by FINSEQ_3:29;
A5: dom (Intervals (f2,r)) = dom f2 by EUCLID_9:def 3;
then len (Intervals (f2,r)) = len f2 by FINSEQ_3:29;
then A6: dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) = dom (Intervals ((f1 ^ f2),r)) by A1, A4, A2, FINSEQ_3:29;

now :: thesis: for i being Nat st i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) holds
((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i

let i be Nat; :: thesis: ( i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) implies ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b₁ = (Intervals ((f1 ^ f2),r)) . b₁ )
assume A7: i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) ; :: thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b₁ = (Intervals ((f1 ^ f2),r)) . b₁
then A8: (Intervals ((f1 ^ f2),r)) . i = ].(((f1 ^ f2) . i) - r),(((f1 ^ f2) . i) + r).[ by A1, A6, EUCLID_9:def 3;

per cases ( i in dom (Intervals (f1,r)) or ex j being Nat st
( j in dom (Intervals (f2,r)) & i = (len (Intervals (f1,r))) + j ) ) by A7, FINSEQ_1:25;

suppose A9: i in dom (Intervals (f1,r)) ; :: thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b₁ = (Intervals ((f1 ^ f2),r)) . b₁

then ( ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals (f1,r)) . i & (f1 ^ f2) . i = f1 . i ) by A3, FINSEQ_1:def 7;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by A3, A8, A9, EUCLID_9:def 3; :: thesis: verum

end;

suppose ex j being Nat st
( j in dom (Intervals (f2,r)) & i = (len (Intervals (f1,r))) + j ) ; :: thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b₁ = (Intervals ((f1 ^ f2),r)) . b₁

then consider j being Nat such that
A10: j in dom (Intervals (f2,r)) and
A11: i = (len (Intervals (f1,r))) + j ;
( ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals (f2,r)) . j & (f1 ^ f2) . i = f2 . j ) by A5, A4, A10, A11, FINSEQ_1:def 7;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by A5, A8, A10, EUCLID_9:def 3; :: thesis: verum

end;

end;

end;

hence (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r) by A6, FINSEQ_1:13; :: thesis: verum