let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
let F be Element of QC-WFF A; :: thesis: rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
thus rng (list_of_immediate_constituents F) c= { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } :: according to XBOOLE_0:def 10 :: thesis: { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (list_of_immediate_constituents F) or y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } )
assume A1: y in rng (list_of_immediate_constituents F) ; :: thesis: y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
rng (list_of_immediate_constituents F) c= QC-WFF A by FINSEQ_1:def 4;
then reconsider G = y as Element of QC-WFF A by A1;
ex x being object st
( x in dom (list_of_immediate_constituents F) & y = (list_of_immediate_constituents F) . x ) by A1, FUNCT_1:def 3;
then G is_immediate_constituent_of F by Th3;
hence y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; :: thesis: verum

end;

thus { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } or x in rng (list_of_immediate_constituents F) )
assume x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; :: thesis: x in rng (list_of_immediate_constituents F)
then consider G being Element of QC-WFF A such that
A2: x = G and
A3: G is_immediate_constituent_of F ;
ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

proof

A4: F <> VERUM A by A3, QC_LANG2:41;

per cases ( F is negative or F is conjunctive or F is universal ) by A3, A4, QC_LANG1:9, QC_LANG2:47;

suppose F is negative ; :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

then A5: ( list_of_immediate_constituents F = <*(the_argument_of F)*> & G = the_argument_of F ) by A3, Def1, QC_LANG2:48;
consider n being Nat such that
A6: n = 1 ;
( dom <*(the_argument_of F)*> = Seg 1 & <*(the_argument_of F)*> . n = the_argument_of F ) by A6, FINSEQ_1:def 8;
hence ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A6, A5, FINSEQ_1:3; :: thesis: verum

end;

suppose A7: F is conjunctive ; :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

A8: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F ;
len <*(the_left_argument_of F),(the_right_argument_of F)*> = 2 by FINSEQ_1:44;
then A9: dom <*(the_left_argument_of F),(the_right_argument_of F)*> = Seg 2 by FINSEQ_1:def 3;
A10: list_of_immediate_constituents F = <*(the_left_argument_of F),(the_right_argument_of F)*> by A7, Def1;
A11: <*(the_left_argument_of F),(the_right_argument_of F)*> . 1 = the_left_argument_of F ;

now :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

per cases ( G = the_left_argument_of F or G = the_right_argument_of F ) by A3, A7, QC_LANG2:49;

suppose A12: G = the_left_argument_of F ; :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

1 in {1,2} by TARSKI:def 2;
hence ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A11, A9, A12, FINSEQ_1:2; :: thesis: verum

end;

suppose G = the_right_argument_of F ; :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

hence ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A8, A9, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

hence ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) ; :: thesis: verum

end;

suppose A13: F is universal ; :: thesis: ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )

then A14: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A13, QC_LANG1:20;
then A15: list_of_immediate_constituents F = <*(the_scope_of F)*> by A14, Def1, A4;
consider n being Nat such that
A16: n = 1 ;
A17: G = the_scope_of F by A3, A13, QC_LANG2:50;
( dom <*(the_scope_of F)*> = Seg 1 & <*(the_scope_of F)*> . n = the_scope_of F ) by A16, FINSEQ_1:def 8;
hence ex n being Nat st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A15, A16, A17, FINSEQ_1:3; :: thesis: verum

end;

end;

end;

hence x in rng (list_of_immediate_constituents F) by A2, FUNCT_1:def 3; :: thesis: verum

end;