set LH = { F3(x) where x is Element of F1() : x in F1() } ;
set RH = { F3(x) where x is Element of F2() : x in F1() } ;
now for y being object st y in { F3(x) where x is Element of F1() : x in F1() } holds
y in { F3(x) where x is Element of F2() : x in F1() } let y be
object ;
( y in { F3(x) where x is Element of F1() : x in F1() } implies y in { F3(x) where x is Element of F2() : x in F1() } )assume
y in { F3(x) where x is Element of F1() : x in F1() }
;
y in { F3(x) where x is Element of F2() : x in F1() } then consider x being
Element of
F1()
such that A2:
(
y = F3(
x) &
x in F1() )
;
reconsider xx =
x as
Element of
F2()
by A2, A1;
(
y = F3(
xx) &
xx in F1() )
by A2;
hence
y in { F3(x) where x is Element of F2() : x in F1() }
;
verum end;
then A3:
{ F3(x) where x is Element of F1() : x in F1() } c= { F3(x) where x is Element of F2() : x in F1() }
;
now for y being object st y in { F3(x) where x is Element of F2() : x in F1() } holds
y in { F3(x) where x is Element of F1() : x in F1() } let y be
object ;
( y in { F3(x) where x is Element of F2() : x in F1() } implies y in { F3(x) where x is Element of F1() : x in F1() } )assume
y in { F3(x) where x is Element of F2() : x in F1() }
;
y in { F3(x) where x is Element of F1() : x in F1() } then consider x being
Element of
F2()
such that A4:
(
y = F3(
x) &
x in F1() )
;
reconsider xx =
x as
Element of
F1()
by A4;
thus
y in { F3(x) where x is Element of F1() : x in F1() }
by A4;
verum end;
then
{ F3(x) where x is Element of F2() : x in F1() } c= { F3(x) where x is Element of F1() : x in F1() }
;
hence
{ F3(x) where x is Element of F1() : x in F1() } = { F3(x) where x is Element of F2() : x in F1() }
by A3; verum