let p, q be ZF-formula; :: thesis: ( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q )
p => q is conditional ;
then p => q = (the_antecedent_of (p => q)) => (the_consequent_of (p => q)) by ZF_LANG:47;
hence ( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q ) by ZF_LANG:32; :: thesis: verum