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 A1: ( k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k ) ; :: thesis: G is_immediate_constituent_of F
A2: F <> VERUM by A1, Def1, RELAT_1:60;
A3: not F is atomic by A1, Def1, RELAT_1:60;

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

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:4, TARSKI:def 1;
then G = the_argument_of F by A1, A5, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A4, QC_LANG2:65; :: thesis: verum

end;

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

then ( not F = VERUM & not F is atomic & not F is negative & not F is conjunctive ) by QC_LANG1:51;
then A7: list_of_immediate_constituents F = <*(the_scope_of F)*> by Def1;
then k in Seg 1 by A1, FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:4, TARSKI:def 1;
then G = the_scope_of F by A1, A7, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A6, QC_LANG2:67; :: thesis: verum

end;

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

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

now

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

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

hence G is_immediate_constituent_of F by A1, A8, A9, A10, QC_LANG2:66; :: thesis: verum

end;

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

hence G is_immediate_constituent_of F by A1, A8, A9, A10, QC_LANG2:66; :: thesis: verum

end;

end;

end;

hence G is_immediate_constituent_of F ; :: thesis: verum

end;

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

then ( not F = VERUM & not F is atomic & not F is negative & not F is conjunctive ) by QC_LANG1:51;
then A13: list_of_immediate_constituents F = <*(the_scope_of F)*> by Def1;
then k in Seg 1 by A1, FINSEQ_1:def 8;
then k = 1 by FINSEQ_1:4, TARSKI:def 1;
then G = the_scope_of F by A1, A13, FINSEQ_1:def 8;
hence G is_immediate_constituent_of F by A12, QC_LANG2:67; :: thesis: verum

end;

end;