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] } :: according to XBOOLE_0:def 10 :: thesis: (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 set ; :: according to TARSKI:def 3 :: thesis: ( 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] } ; :: thesis: 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
A: ( x = f & P1[f] ) ;
ZZ: f in Funcs (F1(),F2()) by FUNCT_2:11, AA;
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] } ; :: thesis: contradiction
then ex g being Function of F1(),F2() st
( f = g & P1[g] ) ;
hence contradiction by A; :: thesis: verum
end;
hence x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } by ZZ, XBOOLE_0:def 5, A; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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 DD: x in (Funcs (F1(),F2())) \ { f where f is Function of F1(),F2() : P1[f] } ; :: thesis: x in { f where f is Function of F1(),F2() : P1[f] }
then CC: x is Function of F1(),F2() by FUNCT_2:121;
not x in { f where f is Function of F1(),F2() : P1[f] } by DD, XBOOLE_0:def 5;
then P1[x] by CC;
hence x in { f where f is Function of F1(),F2() : P1[f] } by CC; :: thesis: verum