let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds
( ( ((@ F) . 1) `1 = 0 implies F = VERUM A ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )
let F be Element of QC-WFF A; :: thesis: ( ( ((@ F) . 1) `1 = 0 implies F = VERUM A ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) )

A1: now :: thesis: ( ( F is atomic & ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A ) or ( F = VERUM A & ((@ F) . 1) `1 = 0 ) or ( F is negative & ((@ F) . 1) `1 = 1 ) or ( F is conjunctive & ((@ F) . 1) `1 = 2 ) or ( F is universal & ((@ F) . 1) `1 = 3 ) )

per cases ( F is atomic or F = VERUM A or F is negative or F is conjunctive or F is universal ) by Th9;

case 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
A2: F = P ! ll ;
@ F = <*P*> ^ ll by A2, 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;

case F = VERUM A ; :: thesis: ((@ F) . 1) `1 = 0

hence ((@ F) . 1) `1 = [0,0] `1
.= 0 ;
:: thesis: verum

end;

case 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;

case F is conjunctive ; :: thesis: ((@ F) . 1) `1 = 2

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

end;

case 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
A4: F = All (x,p) ;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:32;
then (@ F) . 1 = [3,0] by FINSEQ_1:41;
hence ((@ F) . 1) `1 = 3 ; :: thesis: verum

end;

end;

end;

now :: thesis: for k being Nat
for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )

let k be Nat; :: thesis: for P being QC-pred_symbol of k,A holds
( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
let P be QC-pred_symbol of k,A; :: thesis: ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 )
reconsider P9 = P as QC-pred_symbol of A ;
P9 `1 = 7 + (the_arity_of P9) by Def8;
hence ( P `1 <> 0 & P `1 <> 1 & P `1 <> 2 & P `1 <> 3 ) by NAT_1:11; :: thesis: verum

end;

hence ( ( ((@ F) . 1) `1 = 0 implies F = VERUM A ) & ( ((@ F) . 1) `1 = 1 implies F is negative ) & ( ((@ F) . 1) `1 = 2 implies F is conjunctive ) & ( ((@ F) . 1) `1 = 3 implies F is universal ) & ( ex k being Nat st (@ F) . 1 is QC-pred_symbol of k,A implies F is atomic ) ) by A1; :: thesis: verum