set X = { F6(i) where i is Element of F1() : i in rng F4() } ;
set Y = { F6(j) where j is Element of F1() : j in rng (F4() +* (F5(),F2())) } ;
thus
{ F6(i) where i is Element of F1() : i in rng F4() } c= { F6(j) where j is Element of F1() : j in rng (F4() +* (F5(),F2())) }
XBOOLE_0:def 10 { F6(j) where j is Element of F1() : j in rng (F4() +* (F5(),F2())) } c= { F6(i) where i is Element of F1() : i in rng F4() }
let e be object ; TARSKI:def 3 ( not e in { F6(j) where j is Element of F1() : j in rng (F4() +* (F5(),F2())) } or e in { F6(i) where i is Element of F1() : i in rng F4() } )
assume
e in { F6(j) where j is Element of F1() : j in rng (F4() +* (F5(),F2())) }
; e in { F6(i) where i is Element of F1() : i in rng F4() }
then consider j being Element of F1() such that
A8:
e = F6(j)
and
A9:
j in rng (F4() +* (F5(),F2()))
;
consider y being object such that
A10:
y in dom (F4() +* (F5(),F2()))
and
A11:
(F4() +* (F5(),F2())) . y = j
by A9, FUNCT_1:def 3;
A12:
y in dom F4()
by A10, Th29;
then A13:
F4() . y in rng F4()
by FUNCT_1:3;
now e = F6((F4() . y))end;
hence
e in { F6(i) where i is Element of F1() : i in rng F4() }
by A13; verum