let f, g, h, i be ExtReal; {f,g} ++ {h,i} = {(f + h),(f + i),(g + h),(g + i)}
thus {f,g} ++ {h,i} =
({f} \/ {g}) ++ {h,i}
by ENUMSET1:1
.=
({f} ++ {h,i}) \/ ({g} ++ {h,i})
by Th41
.=
{(f + h),(f + i)} \/ ({g} ++ {h,i})
by Th44
.=
{(f + h),(f + i)} \/ {(g + h),(g + i)}
by Th44
.=
{(f + h),(f + i),(g + h),(g + i)}
by ENUMSET1:5
; verum