let S be Language; :: thesis: AllFormulasOf S is S -prefix
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;

now :: thesis: for p1, q1, p2, q2 being AllSymbolsOf S -valued FinSequence st p1 in AllFormulasOf S & p2 in AllFormulasOf S & p1 ^ q1 = p2 ^ q2 holds
( p1 = p2 & q1 = q2 )

let p1, q1, p2, q2 be AllSymbolsOf S -valued FinSequence; :: thesis: ( p1 in AllFormulasOf S & p2 in AllFormulasOf S & p1 ^ q1 = p2 ^ q2 implies ( p1 = p2 & q1 = q2 ) )
assume A1: ( p1 in AllFormulasOf S & p2 in AllFormulasOf S & p1 ^ q1 = p2 ^ q2 ) ; :: thesis: ( p1 = p2 & q1 = q2 )
then reconsider phi1 = p1, phi2 = p2 as wff string of S ;
consider m1 being Nat such that
A2: phi1 is m1 -wff by Def24;
consider m2 being Nat such that
A3: phi2 is m2 -wff by Def24;
set N = m1 + m2;
set PhiN = S -formulasOfMaxDepth (m1 + m2);
( phi1 is m1 + (0 * m2) -wff & phi2 is m2 + (0 * m1) -wff ) by A2, A3;
then reconsider phi11 = phi1, phi22 = phi2 as m1 + m2 -wff string of S ;
( phi11 in S -formulasOfMaxDepth (m1 + m2) & phi22 in S -formulasOfMaxDepth (m1 + m2) ) by Def23;
hence ( p1 = p2 & q1 = q2 ) by A1, FOMODEL0:def 19; :: thesis: verum

end;

then AllFormulasOf S is AllSymbolsOf S -prefix ;
hence AllFormulasOf S is S -prefix ; :: thesis: verum