let f, g be ExtReal; :: thesis: {f,g} "" = {(f "),(g ")}
thus {f,g} "" = ({f} \/ {g}) "" by ENUMSET1:1
.= ({f} "") \/ ({g} "") by Th23
.= {(f ")} \/ ({g} "") by Th26
.= {(f ")} \/ {(g ")} by Th26
.= {(f "),(g ")} by ENUMSET1:1 ; :: thesis: verum