let F be Element of QC-WFF ; :: thesis:
thus ((@ VERUM ) . 1) `1 = [0 ,0 ] `1 by FINSEQ_1:def 8
.= 0 by MCART_1:7 ; :: thesis:
thus ( F is atomic implies ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k ) :: thesis:

assume F is atomic ; :: thesis:
then consider k being Element of NAT , P being QC-pred_symbol of k, ll being QC-variable_list of such that
A1: F = P ! ll by Def17;
@ F = <*P*> ^ ll by A1, Th23;
then (@ F) . 1 = P by FINSEQ_1:58;
hence ex k being Element of NAT st (@ F) . 1 is QC-pred_symbol of k ; :: thesis:

end;

thus ( F is negative implies ((@ F) . 1) `1 = 1 ) :: thesis:

assume F is negative ; :: thesis:
then consider p being Element of QC-WFF such that
A2: F = 'not' p by Def18;
(@ F) . 1 = [1,0 ] by A2, FINSEQ_1:58;
hence ((@ F) . 1) `1 = 1 by MCART_1:7; :: thesis:

end;

thus ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) :: thesis:

assume F is conjunctive ; :: thesis:
then consider p, q being Element of QC-WFF such that
A3: F = p '&' q by Def19;
@ F = <*[2,0 ]*> ^ ((@ p) ^ (@ q)) by A3, FINSEQ_1:45;
then (@ F) . 1 = [2,0 ] by FINSEQ_1:58;
hence ((@ F) . 1) `1 = 2 by MCART_1:7; :: thesis:

end;

thus ( F is universal implies ((@ F) . 1) `1 = 3 ) :: thesis:

assume F is universal ; :: thesis:
then consider x being bound_QC-variable, p being Element of QC-WFF such that
A4: F = All x,p by Def20;
@ F = <*[3,0 ]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:45;
then (@ F) . 1 = [3,0 ] by FINSEQ_1:58;
hence ((@ F) . 1) `1 = 3 by MCART_1:7; :: thesis:

end;