let IT1, IT2 be set ; :: thesis: ( ( not phi is 0wff & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & IT1 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & IT2 = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p ) implies IT1 = IT2 ) & ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 ) )
thus ( not phi is 0wff & S₁[IT1] & S₁[IT2] implies IT1 = IT2 ) :: thesis: ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 )

proof

assume not phi is 0wff ; :: thesis: ( not S₁[IT1] or not S₁[IT2] or IT1 = IT2 )
then reconsider phi = phi as non 0wff string of S ;
assume C0: ( S₁[IT1] & S₁[IT2] ) ; :: thesis: IT1 = IT2
consider phi1 being wff string of S, p1 being FinSequence such that
B1: ( p1 is AllSymbolsOf S -valued & IT1 = [phi1,p1] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p1 ) by C0;
consider phi2 being wff string of S, p2 being FinSequence such that
B2: ( p2 is AllSymbolsOf S -valued & IT2 = [phi2,p2] & phi = (<*((S -firstChar) . phi)*> ^ phi2) ^ p2 ) by C0;
reconsider q1 = p1, q2 = p2 as AllSymbolsOf S -valued FinSequence by B1, B2;
<*((S -firstChar) . phi)*> ^ (phi1 ^ p1) = phi by B1, FINSEQ_1:32
.= <*((S -firstChar) . phi)*> ^ (phi2 ^ p2) by B2, FINSEQ_1:32 ;
then ( phi1 ^ q1 = phi2 ^ q2 & phi1 in AllFormulasOf S & phi2 in AllFormulasOf S ) by Th16, FINSEQ_1:33;
then ( phi1 = phi2 & q1 = q2 ) by FOMODEL0:def 20;
hence IT1 = IT2 by B1, B2; :: thesis: verum

end;

thus ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 ) ; :: thesis: verum