theorem :: ZF_LANG1:178

for H being ZF-formula
for x, y being Variable st H is disjunctive holds
( the_left_argument_of (H / (x,y)) = (the_left_argument_of H) / (x,y) & the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )