consider m being Nat such that
A1: m1 = m + 1 by NAT_1:6;
set phi = the m -wff string of S;
set l = the literal Element of S;
set psi = <* the literal Element of S*> ^ the m -wff string of S;
reconsider psii = <* the literal Element of S*> ^ the m -wff string of S as m1 -wff string of S by A1;
take psii ; :: thesis: psii is exal
thus psii is exal ; :: thesis: verum