let p, q be ZF-formula; :: thesis: Free (p '&' q) = (Free p) \/ (Free q)
A1: the_right_argument_of (p '&' q) = q by Th4;
( p '&' q is conjunctive & the_left_argument_of (p '&' q) = p ) by Th4;
hence Free (p '&' q) = (Free p) \/ (Free q) by A1, ZF_MODEL:1; :: thesis: verum