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 = (<*(() . phi)*> ^ phi1) ^ p ) & ex phi1 being wff string of S ex p being FinSequence st
( p is AllSymbolsOf S -valued & IT2 = [phi1,p] & phi = (<*(() . phi)*> ^ phi1) ^ p ) implies IT1 = IT2 ) & ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 ) )

thus ( not phi is 0wff & S1[IT1] & S1[IT2] implies IT1 = IT2 ) :: thesis: ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 )
proof
assume not phi is 0wff ; :: thesis: ( not S1[IT1] or not S1[IT2] or IT1 = IT2 )
then reconsider phi = phi as non 0wff string of S ;
assume A6: ( S1[IT1] & S1[IT2] ) ; :: thesis: IT1 = IT2
consider phi1 being wff string of S, p1 being FinSequence such that
A7: ( p1 is AllSymbolsOf S -valued & IT1 = [phi1,p1] & phi = (<*(() . phi)*> ^ phi1) ^ p1 ) by A6;
consider phi2 being wff string of S, p2 being FinSequence such that
A8: ( p2 is AllSymbolsOf S -valued & IT2 = [phi2,p2] & phi = (<*(() . phi)*> ^ phi2) ^ p2 ) by A6;
reconsider q1 = p1, q2 = p2 as AllSymbolsOf S -valued FinSequence by A7, A8;
<*(() . phi)*> ^ (phi1 ^ p1) = phi by
.= <*(() . phi)*> ^ (phi2 ^ p2) by ;
then ( phi1 ^ q1 = phi2 ^ q2 & phi1 in AllFormulasOf S & phi2 in AllFormulasOf S ) by ;
then ( phi1 = phi2 & q1 = q2 ) by FOMODEL0:def 19;
hence IT1 = IT2 by A7, A8; :: thesis: verum
end;
thus ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 ) ; :: thesis: verum