set X = { F₆(i) where i is Element of F₁() : i in rng F₄() } ;
set Y = { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } ;
thus { F₆(i) where i is Element of F₁() : i in rng F₄() } c= { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } :: according to XBOOLE_0:def 10 :: thesis: { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } c= { F₆(i) where i is Element of F₁() : i in rng F₄() }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { F₆(i) where i is Element of F₁() : i in rng F₄() } or e in { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } )
assume e in { F₆(i) where i is Element of F₁() : i in rng F₄() } ; :: thesis: e in { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) }
then consider j being Element of F₁() such that
A3: e = F₆(j) and
A4: j in rng F₄() ;
consider y being object such that
A5: y in dom F₄() and
A6: F₄() . y = j by A4, FUNCT_1:def 3;
y in dom (F₄() +* (F₅(),F₂())) by A5, Th29;
then A7: (F₄() +* (F₅(),F₂())) . y in rng (F₄() +* (F₅(),F₂())) by FUNCT_1:3;

now :: thesis: e = F₆(((F₄() +* (F₅(),F₂())) . y))

per cases ( y = F₅() or y <> F₅() ) ;

suppose y = F₅() ; :: thesis: e = F₆(((F₄() +* (F₅(),F₂())) . y))

hence e = F₆(((F₄() +* (F₅(),F₂())) . y)) by A1, A2, A3, A6, Th30, A5; :: thesis: verum

end;

suppose y <> F₅() ; :: thesis: e = F₆(((F₄() +* (F₅(),F₂())) . y))

hence e = F₆(((F₄() +* (F₅(),F₂())) . y)) by A3, Th31, A6; :: thesis: verum

end;

end;

end;

hence e in { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } by A7; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } or e in { F₆(i) where i is Element of F₁() : i in rng F₄() } )
assume e in { F₆(j) where j is Element of F₁() : j in rng (F₄() +* (F₅(),F₂())) } ; :: thesis: e in { F₆(i) where i is Element of F₁() : i in rng F₄() }
then consider j being Element of F₁() such that
A8: e = F₆(j) and
A9: j in rng (F₄() +* (F₅(),F₂())) ;
consider y being object such that
A10: y in dom (F₄() +* (F₅(),F₂())) and
A11: (F₄() +* (F₅(),F₂())) . y = j by A9, FUNCT_1:def 3;
A12: y in dom F₄() by A10, Th29;
then A13: F₄() . y in rng F₄() by FUNCT_1:3;

now :: thesis: e = F₆((F₄() . y))

per cases ( y = F₅() or y <> F₅() ) ;

suppose y = F₅() ; :: thesis: e = F₆((F₄() . y))

hence e = F₆((F₄() . y)) by A1, A2, A8, A11, Th30, A12; :: thesis: verum

end;

suppose y <> F₅() ; :: thesis: e = F₆((F₄() . y))

hence e = F₆((F₄() . y)) by A8, Th31, A11; :: thesis: verum

end;

end;

end;

hence e in { F₆(i) where i is Element of F₁() : i in rng F₄() } by A13; :: thesis: verum