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 PARTIT_2:def 1
.= id (E ^omega) ;
hence Lang (w,(id (E ^omega))) = Lang (w,({} ((E ^omega),(E ^omega)))) by Th49
.= {w} by Th50 ;
:: thesis: verum