let f be non constant standard special_circular_sequence; :: thesis: (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `))
(L~ f) ` = [#] ((TOP-REAL 2) | ((L~ f) `)) by PRE_TOPC:def 5
.= the carrier of ((TOP-REAL 2) | ((L~ f) `)) ;
hence (L~ f) ` = the carrier of ((TOP-REAL 2) | ((L~ f) `)) ; :: thesis: verum