let H be ZF-formula; :: thesis: 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) )
let x, y be Variable; :: thesis: ( H is disjunctive implies ( 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) ) )
assume A1: H is disjunctive ; :: thesis: ( 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) )
then H / (x,y) is disjunctive by Th174;
then A2: H / (x,y) = (the_left_argument_of (H / (x,y))) 'or' (the_right_argument_of (H / (x,y))) by ZF_LANG:41;
H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1, ZF_LANG:41;
hence ( 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) ) by A2, Th161; :: thesis: verum