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

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