set z1 = { f where f is Function of F1(),F2() : P1[f] } ;
set z2 = { f where f is Function of F1(),F2() : P1[f] } ;
set zc = Funcs (F1(),F2());
thus
{ f where f is Function of F1(),F2() : P1[f] } c= (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
XBOOLE_0:def 10 (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } c= { f where f is Function of F1(),F2() : P1[f] } proof
let x be
object ;
TARSKI:def 3 ( not x in { f where f is Function of F1(),F2() : P1[f] } or x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } )
assume
x in { f where f is Function of F1(),F2() : P1[f] }
;
x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
then consider f being
Function of
F1(),
F2()
such that A2:
(
x = f &
P1[
f] )
;
A3:
f in Funcs (
F1(),
F2())
by A1, FUNCT_2:8;
not
f in { f where f is Function of F1(),F2() : P1[f] }
proof
assume
f in { f where f is Function of F1(),F2() : P1[f] }
;
contradiction
then
ex
g being
Function of
F1(),
F2() st
(
f = g &
P1[
g] )
;
hence
contradiction
by A2;
verum
end;
hence
x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
by A3, A2, XBOOLE_0:def 5;
verum
end;
let x be object ; TARSKI:def 3 ( not x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } or x in { f where f is Function of F1(),F2() : P1[f] } )
assume A4:
x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] }
; x in { f where f is Function of F1(),F2() : P1[f] }
then A5:
x is Function of F1(),F2()
by FUNCT_2:66;
not x in { f where f is Function of F1(),F2() : P1[f] }
by A4, XBOOLE_0:def 5;
then
P1[x]
by A5;
hence
x in { f where f is Function of F1(),F2() : P1[f] }
by A5; verum