let k be Element of NAT ; :: thesis: for F, G being Element of QC-WFF st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
let F, G be Element of QC-WFF ; :: thesis: ( k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k implies G is_immediate_constituent_of F )
assume that
A1: k in dom (list_of_immediate_constituents F) and
A2: G = (list_of_immediate_constituents F) . k ; :: thesis: G is_immediate_constituent_of F
A3: ( F <> VERUM & not F is atomic ) by A1, Def1, RELAT_1:38;

per cases ( F is negative or F is universal or F is conjunctive or F is universal ) by A3, QC_LANG1:7;

suppose A4: F is negative ; :: thesis: G is_immediate_constituent_of F

then A5: 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, A5, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A4, QC_LANG2:48; :: thesis: verum

end;

suppose A6: F is universal ; :: thesis: G is_immediate_constituent_of F

then A7: not F is conjunctive by QC_LANG1:18;
( not F is atomic & not F is negative ) by A6, QC_LANG1:18;
then A8: list_of_immediate_constituents F = <*(the_scope_of F)*> by A6, A7, Def1, QC_LANG1:18;
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, A8, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A6, QC_LANG2:50; :: thesis: verum

end;

suppose A9: F is conjunctive ; :: thesis: G is_immediate_constituent_of F

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

now

per cases ( k = 1 or k = 2 ) by A13, TARSKI:def 2;

suppose k = 1 ; :: thesis: G is_immediate_constituent_of F

hence G is_immediate_constituent_of F by A2, A9, A12, A11, QC_LANG2:49; :: thesis: verum

end;

suppose k = 2 ; :: thesis: G is_immediate_constituent_of F

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

end;

end;

end;

hence G is_immediate_constituent_of F ; :: thesis: verum

end;

suppose A14: F is universal ; :: thesis: G is_immediate_constituent_of F

then A15: not F is conjunctive by QC_LANG1:18;
( not F is atomic & not F is negative ) by A14, QC_LANG1:18;
then A16: list_of_immediate_constituents F = <*(the_scope_of F)*> by A14, A15, Def1, QC_LANG1:18;
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, A16, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A14, QC_LANG2:50; :: thesis: verum

end;

end;