let p, q be boolean-valued Function; :: thesis: for x being set st x in (dom p) /\ (dom q) holds
( (p 'or' q) . x = TRUE iff ( p . x = TRUE or q . x = TRUE ) )
let x be set ; :: thesis: ( x in (dom p) /\ (dom q) implies ( (p 'or' q) . x = TRUE iff ( p . x = TRUE or q . x = TRUE ) ) )
assume A1: x in (dom p) /\ (dom q) ; :: thesis: ( (p 'or' q) . x = TRUE iff ( p . x = TRUE or q . x = TRUE ) )
A2: x in dom (p 'or' q) by A1, BVFUNC_1:def 2;
then A3: (p 'or' q) . x = (p . x) 'or' (q . x) by BVFUNC_1:def 2;

hereby :: thesis: ( ( p . x = TRUE or q . x = TRUE ) implies (p 'or' q) . x = TRUE )

assume (p 'or' q) . x = TRUE ; :: thesis: ( p . x = TRUE or q . x = TRUE )
then (p . x) 'or' (q . x) = TRUE by A2, BVFUNC_1:def 2;
then ( 'not' (p . x) = FALSE or 'not' (q . x) = FALSE ) ;
hence ( p . x = TRUE or q . x = TRUE ) ; :: thesis: verum

end;

assume ( p . x = TRUE or q . x = TRUE ) ; :: thesis: (p 'or' q) . x = TRUE
hence (p 'or' q) . x = TRUE by A3; :: thesis: verum