let IT1, IT2 be set ; ( ( 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 & S1[IT1] & S1[IT2] implies IT1 = IT2 )
( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 )proof
assume
not
phi is
0wff
;
( 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] )
;
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;
verum
end;
thus
( phi is 0wff & IT1 = [phi,{}] & IT2 = [phi,{}] implies IT1 = IT2 )
; verum