let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds
( ((@ (VERUM A)) . 1) `1 = 0 & ( F is atomic implies ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ) & ( F is negative implies ((@ F) . 1) `1 = 1 ) & ( F is conjunctive implies ((@ F) . 1) `1 = 2 ) & ( F is universal implies ((@ F) . 1) `1 = 3 ) )
let F be Element of QC-WFF A; :: thesis: ( ((@ (VERUM A)) . 1) `1 = 0 & ( F is atomic implies ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ) & ( 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 A)) . 1) `1 = [0,0] `1
.= 0 ; :: thesis: ( ( F is atomic implies ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ) & ( 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 Nat st (@ F) . 1 is QC-pred_symbol of k,A ) :: 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 Nat st (@ F) . 1 is QC-pred_symbol of k,A
then consider k being Nat, P being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A1: F = P ! ll ;
@ F = <*P*> ^ ll by A1, Th8;
then (@ F) . 1 = P by FINSEQ_1:41;
hence ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ; :: 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 A st F = 'not' p ;
then (@ F) . 1 = [1,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 1 ; :: 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 A such that
A2: F = p '&' q ;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A2, FINSEQ_1:32;
then (@ F) . 1 = [2,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 2 ; :: 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 of A, p being Element of QC-WFF A such that
A3: F = All (x,p) ;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A3, FINSEQ_1:32;
then (@ F) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 3 ; :: thesis: verum

end;