let f, g be ext-real number ; :: thesis: {f,g} "" = {(f " ),(g " )}
thus {f,g} "" = ({f} \/ {g}) "" by ENUMSET1:41
.= ({f} "" ) \/ ({g} "" ) by Th23
.= {(f " )} \/ ({g} "" ) by Th26
.= {(f " )} \/ {(g " )} by Th26
.= {(f " ),(g " )} by ENUMSET1:41 ; :: thesis: verum