let A be QC-alphabet ; :: 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