let Iac, Icb be non empty closed_interval Subset of REAL; :: thesis: for Dac being Division of Iac
for Dcb being Division of Icb st upper_bound Iac = lower_bound Icb & len Dcb = 1 & Dcb . 1 = lower_bound Icb holds
Dac (#) Dcb = Dac
let Dac be Division of Iac; :: thesis: for Dcb being Division of Icb st upper_bound Iac = lower_bound Icb & len Dcb = 1 & Dcb . 1 = lower_bound Icb holds
Dac (#) Dcb = Dac
let Dcb be Division of Icb; :: thesis: ( upper_bound Iac = lower_bound Icb & len Dcb = 1 & Dcb . 1 = lower_bound Icb implies Dac (#) Dcb = Dac )
assume that
A1: upper_bound Iac = lower_bound Icb and
A2: len Dcb = 1 and
A3: Dcb . 1 = lower_bound Icb ; :: thesis: Dac (#) Dcb = Dac
len (Dcb /^ 1) = (len Dcb) - 1 by A2, RFINSEQ:def 1;
then Dcb /^ 1 = {} by A2;
then Dac ^ (Dcb /^ 1) = Dac by FINSEQ_1:34;
hence Dac (#) Dcb = Dac by A1, A3, Def4; :: thesis: verum