take f = pr1 S,the carrier of A; :: thesis: ( f is complying_with_empty-instruction & f is complying_with_catenation & f complies_with_if_wrt T & f complies_with_while_wrt T )
thus ( f is complying_with_empty-instruction & f is complying_with_catenation & f complies_with_if_wrt T & f complies_with_while_wrt T ) by Th81; :: thesis: verum