let E be set ; :: thesis: for w being Element of E ^omega holds Lang w,(id (E ^omega )) = {w}
let w be Element of E ^omega ; :: thesis: Lang w,(id (E ^omega )) = {w}
({} (E ^omega ),(E ^omega )) \/ (id (E ^omega )) = {} \/ (id (E ^omega )) by OPOSET_1:def 1
.= id (E ^omega ) ;
hence Lang w,(id (E ^omega )) = Lang w,({} (E ^omega ),(E ^omega )) by Th49
.= {w} by Th50 ;
:: thesis: verum