set X = { F4(j) where j is Element of F1() : j in {F2(),F3()} } ;
for x being object holds
( x in F4(F2()) \/ F4(F3()) iff ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) )
proof
let x be
object ;
( x in F4(F2()) \/ F4(F3()) iff ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) )
thus
(
x in F4(
F2())
\/ F4(
F3()) implies ex
Y being
set st
(
x in Y &
Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) )
( ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } ) implies x in F4(F2()) \/ F4(F3()) )proof
assume
x in F4(
F2())
\/ F4(
F3())
;
ex Y being set st
( x in Y & Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} } )
end;
given Y being
set such that A3:
x in Y
and A4:
Y in { F4(j) where j is Element of F1() : j in {F2(),F3()} }
;
x in F4(F2()) \/ F4(F3())
consider j being
Element of
F1()
such that A5:
Y = F4(
j)
and A6:
j in {F2(),F3()}
by A4;
now ( ( j = F2() & x in F4(F2()) ) or ( j = F3() & x in F4(F3()) ) )end;
hence
x in F4(
F2())
\/ F4(
F3())
by XBOOLE_0:def 3;
verum
end;
hence
union { F4(j) where j is Element of F1() : j in {F2(),F3()} } = F4(F2()) \/ F4(F3())
by TARSKI:def 4; verum