let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) /\ ((A ^Foi ) ` )
let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fob ) /\ ((A ^Foi ) ` )
((A ` ) ^Fob ) ` = A ^Foi by Th38;
hence A ^Fodelta = (A ^Fob ) /\ ((A ^Foi ) ` ) by Th40; :: thesis: verum