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

proof

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

end;

thus ( F is negative implies ((@ F) . 1) `1 = 1 ) :: thesis: ( ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) & ( F is universal implies ((@ F) . 1) `1 = 3 ) )

proof

assume F is negative ; :: thesis: ((@ F) . 1) `1 = 1
then ex p being Element of QC-WFF st F = 'not' p by Def18;
then (@ F) . 1 = [1,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 1 by MCART_1:7; :: thesis: verum

end;

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

proof

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

end;

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

proof

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

end;