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