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

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