let A be QC-alphabet ; :: thesis:
let k be Nat; :: thesis:
let F, G be Element of QC-WFF A; :: thesis:
assume that
A1: k in dom (list_of_immediate_constituents F) and
A2: G = (list_of_immediate_constituents F) . k ; :: thesis:
A3: list_of_immediate_constituents F <> <*> (QC-WFF A) by A1;
A4: ( F <> VERUM A & not F is atomic ) by Def1, A3;

per cases by A4, QC_LANG1:9;

suppose A5: F is negative ; :: thesis:

then A6: list_of_immediate_constituents F = <*(the_argument_of F)*> by Def1;
then k in Seg 1 by A1, FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2, TARSKI:def 1;
then G = the_argument_of F by A2, A6, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A5, QC_LANG2:48; :: thesis:

end;

suppose A7: F is universal ; :: thesis:

then A8: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A7, QC_LANG1:20;
then A9: list_of_immediate_constituents F = <*(the_scope_of F)*> by A8, Def1, A4;
then k in Seg 1 by A1, FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2, TARSKI:def 1;
then G = the_scope_of F by A2, A9, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A7, QC_LANG2:50; :: thesis:

end;

suppose A10: F is conjunctive ; :: thesis:

A11: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F by FINSEQ_1:44;
A12: <*(the_left_argument_of F),(the_right_argument_of F)*> . 1 = the_left_argument_of F by FINSEQ_1:44;
A13: list_of_immediate_constituents F = <*(the_left_argument_of F),(the_right_argument_of F)*> by A10, Def1;
len <*(the_left_argument_of F),(the_right_argument_of F)*> = 2 by FINSEQ_1:44;
then A14: k in {1,2} by A1, A13, FINSEQ_1:2, FINSEQ_1:def 3;

per cases by A14, TARSKI:def 2;

suppose k = 1 ; :: thesis:

hence G is_immediate_constituent_of F by A2, A10, A13, A12, QC_LANG2:49; :: thesis:

end;

suppose k = 2 ; :: thesis:

hence G is_immediate_constituent_of F by A2, A10, A13, A11, QC_LANG2:49; :: thesis:

end;

end;

end;

hence G is_immediate_constituent_of F ; :: thesis:

end;

suppose A15: F is universal ; :: thesis:

then A16: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A15, QC_LANG1:20;
then A17: list_of_immediate_constituents F = <*(the_scope_of F)*> by A16, Def1, A4;
then k in Seg 1 by A1, FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:2, TARSKI:def 1;
then G = the_scope_of F by A2, A17, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A15, QC_LANG2:50; :: thesis:

end;

end;