thus { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] } c= { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } :: according to XBOOLE_0:def 10 :: thesis: { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } c= { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] } or x in { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } )
assume x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] } ; :: thesis: x in { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] }
then consider s being Element of F₁(), t being Element of F₂() such that
A2: x = F₃(s,t) and
A3: P₂[s,t] ;
A4: P₁[s,t] by A1, A3;
t = F₄() by A1, A3;
hence x in { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } by A2, A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } or x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] } )
assume x in { F₃(s9,F₄()) where s9 is Element of F₁() : P₁[s9,F₄()] } ; :: thesis: x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] }
then consider s9 being Element of F₁() such that
A5: x = F₃(s9,F₄()) and
A6: P₁[s9,F₄()] ;
P₂[s9,F₄()] by A1, A6;
hence x in { F₃(s,t) where s is Element of F₁(), t is Element of F₂() : P₂[s,t] } by A5; :: thesis: verum