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 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 & H = (the_left_argument_of H) 'or' (the_right_argument_of H) ) by Th188, ZF_LANG:59;
then ( H / x,y = (the_left_argument_of (H / x,y)) 'or' (the_right_argument_of (H / x,y)) & H / x,y = ((the_left_argument_of H) / x,y) 'or' ((the_right_argument_of H) / x,y) ) by Th175, ZF_LANG:59;
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 ZF_LANG:48; :: thesis: verum