let A be QC-alphabet ; :: thesis: for k being Nat
for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
let k be Nat; :: thesis: for F, G being Element of QC-WFF A 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 A; :: 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: list_of_immediate_constituents F <> <*> (QC-WFF A) by A1;
A4: ( F <> VERUM A & not F is atomic ) by Def1, A3;

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

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

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

end;

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

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;
hence G is_immediate_constituent_of F by A7, QC_LANG2:50; :: thesis: verum

end;

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

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;

now :: thesis: G is_immediate_constituent_of F

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

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

hence G is_immediate_constituent_of F by A2, A10, A13, 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, A10, A13, QC_LANG2:49; :: thesis: verum

end;

end;

end;

hence G is_immediate_constituent_of F ; :: thesis: verum

end;

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

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;
hence G is_immediate_constituent_of F by A15, QC_LANG2:50; :: thesis: verum

end;

end;