let S be Element of QC-Sub-WFF ; :: thesis: ( ( S is Sub_VERUM implies ((@ (S `1 )) . 1) `1 = 0 ) & ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1 )) . 1 is QC-pred_symbol of k ) & ( S is Sub_negative implies ((@ (S `1 )) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) )
thus ( S is Sub_VERUM implies ((@ (S `1 )) . 1) `1 = 0 ) :: thesis: ( ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1 )) . 1 is QC-pred_symbol of k ) & ( S is Sub_negative implies ((@ (S `1 )) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) )

proof

assume S is Sub_VERUM ; :: thesis: ((@ (S `1 )) . 1) `1 = 0
then consider e being Element of vSUB such that
A1: S = [VERUM ,e] by Def19;
S `1 = VERUM by A1, MCART_1:7;
hence ((@ (S `1 )) . 1) `1 = [0 ,0 ] `1 by FINSEQ_1:def 8
.= 0 by MCART_1:7 ;
:: thesis: verum

end;

thus ( S is Sub_atomic implies ex k being Element of NAT st (@ (S `1 )) . 1 is QC-pred_symbol of k ) :: thesis: ( ( S is Sub_negative implies ((@ (S `1 )) . 1) `1 = 1 ) & ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) )

proof

assume S is Sub_atomic ; :: thesis: ex k being Element of NAT st (@ (S `1 )) . 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 , e being Element of vSUB such that
A2: S = Sub_P P,ll,e by Def25;
S = [(P ! ll),e] by A2, Th9;
then S `1 = P ! ll by MCART_1:7;
then @ (S `1 ) = <*P*> ^ ll by QC_LANG1:23;
then (@ (S `1 )) . 1 = P by FINSEQ_1:58;
hence ex k being Element of NAT st (@ (S `1 )) . 1 is QC-pred_symbol of k ; :: thesis: verum

end;

thus ( S is Sub_negative implies ((@ (S `1 )) . 1) `1 = 1 ) :: thesis: ( ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) & ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) )

proof

assume S is Sub_negative ; :: thesis: ((@ (S `1 )) . 1) `1 = 1
then consider S' being Element of QC-Sub-WFF such that
A3: S = Sub_not S' by Def26;
S `1 = 'not' (S' `1 ) by A3, MCART_1:7;
then (@ (S `1 )) . 1 = [1,0 ] by FINSEQ_1:58;
hence ((@ (S `1 )) . 1) `1 = 1 by MCART_1:7; :: thesis: verum

end;

thus ( S is Sub_conjunctive implies ((@ (S `1 )) . 1) `1 = 2 ) :: thesis: ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 )

proof

assume S is Sub_conjunctive ; :: thesis: ((@ (S `1 )) . 1) `1 = 2
then consider S1, S2 being Element of QC-Sub-WFF such that
A4: ( S = Sub_& S1,S2 & S1 `2 = S2 `2 ) by Def27;
S = [((S1 `1 ) '&' (S2 `1 )),(S1 `2 )] by A4, Def21;
then S `1 = (S1 `1 ) '&' (S2 `1 ) by MCART_1:7;
then @ (S `1 ) = <*[2,0 ]*> ^ ((@ (S1 `1 )) ^ (@ (S2 `1 ))) by FINSEQ_1:45;
then (@ (S `1 )) . 1 = [2,0 ] by FINSEQ_1:58;
hence ((@ (S `1 )) . 1) `1 = 2 by MCART_1:7; :: thesis: verum

end;

thus ( S is Sub_universal implies ((@ (S `1 )) . 1) `1 = 3 ) :: thesis: verum

proof

assume S is Sub_universal ; :: thesis: ((@ (S `1 )) . 1) `1 = 3
then consider B being Element of [:QC-Sub-WFF ,bound_QC-variables :], SQ being second_Q_comp of B such that
A5: ( S = Sub_All B,SQ & B is quantifiable ) by Def28;
S = [(All (B `2 ),((B `1 ) `1 )),SQ] by A5, Def24;
then S `1 = All (B `2 ),((B `1 ) `1 ) by MCART_1:7;
then @ (S `1 ) = <*[3,0 ]*> ^ (<*(B `2 )*> ^ (@ ((B `1 ) `1 ))) by FINSEQ_1:45;
then (@ (S `1 )) . 1 = [3,0 ] by FINSEQ_1:58;
hence ((@ (S `1 )) . 1) `1 = 3 by MCART_1:7; :: thesis: verum

end;