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 ;
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))) . b1 = (Intervals ((f1 ^ f2),r)) . b1 )
assume A7: i in dom ((Intervals (f1,r)) ^ (Intervals (f2,r))) ; :: thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
then A8: (Intervals ((f1 ^ f2),r)) . i = ].(((f1 ^ f2) . i) - r),(((f1 ^ f2) . i) + r).[ by ;
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 ;
suppose A9: i in dom (Intervals (f1,r)) ; :: thesis: ((Intervals (f1,r)) ^ (Intervals (f2,r))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
then ( ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals (f1,r)) . i & (f1 ^ f2) . i = f1 . i ) by ;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by ; :: 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))) . b1 = (Intervals ((f1 ^ f2),r)) . b1
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 ;
hence ((Intervals (f1,r)) ^ (Intervals (f2,r))) . i = (Intervals ((f1 ^ f2),r)) . i by ; :: thesis: verum
end;
end;
end;
hence (Intervals (f1,r)) ^ (Intervals (f2,r)) = Intervals ((f1 ^ f2),r) by ; :: thesis: verum