let S be Language; :: thesis: AllFormulasOf S is S -prefix

set FF = AllFormulasOf S;

set SS = AllSymbolsOf S;

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

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 )

then
AllFormulasOf S is AllSymbolsOf S -prefix
;( 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;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

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