let p, q be ZF-formula; :: thesis: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
p '&' q is conjunctive ;
then p '&' q = (the_left_argument_of (p '&' q)) '&' (the_right_argument_of (p '&' q)) by ZF_LANG:40;
hence ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by ZF_LANG:30; :: thesis: verum