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_{1}[IT1] & S_{1}[IT2] implies IT1 = IT2 )
:: thesis: ( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 )

( 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

proof

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

then reconsider phi = phi as non 0wff string of S ;

assume A6: ( S_{1}[IT1] & S_{1}[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 = (<*((S -firstChar) . 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 = (<*((S -firstChar) . phi)*> ^ phi2) ^ p2 ) by A6;

reconsider q1 = p1, q2 = p2 as AllSymbolsOf S -valued FinSequence by A7, A8;

<*((S -firstChar) . phi)*> ^ (phi1 ^ p1) = phi by A7, FINSEQ_1:32

.= <*((S -firstChar) . phi)*> ^ (phi2 ^ p2) by FINSEQ_1:32, A8 ;

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 19;

hence IT1 = IT2 by A7, A8; :: thesis: verum

end;then reconsider phi = phi as non 0wff string of S ;

assume A6: ( S

consider phi1 being wff string of S, p1 being FinSequence such that

A7: ( p1 is AllSymbolsOf S -valued & IT1 = [phi1,p1] & phi = (<*((S -firstChar) . 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 = (<*((S -firstChar) . phi)*> ^ phi2) ^ p2 ) by A6;

reconsider q1 = p1, q2 = p2 as AllSymbolsOf S -valued FinSequence by A7, A8;

<*((S -firstChar) . phi)*> ^ (phi1 ^ p1) = phi by A7, FINSEQ_1:32

.= <*((S -firstChar) . phi)*> ^ (phi2 ^ p2) by FINSEQ_1:32, A8 ;

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 19;

hence IT1 = IT2 by A7, A8; :: thesis: verum