let x be set ; for S being Language
for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )
let S be Language; for p2 being FinSequence
for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )
let p2 be FinSequence; for phi, phi2 being wff string of S st not phi is 0wff holds
( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )
let phi, phi2 be wff string of S; ( not phi is 0wff implies ( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) ) )
set Phi = SubWffsOf phi;
set F = S -firstChar ;
set s = (S -firstChar) . phi;
set SS = AllSymbolsOf S;
assume A1:
not phi is 0wff
; ( phi = (<*x*> ^ phi2) ^ p2 iff ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi ) )
then consider phi1 being wff string of S, p being FinSequence such that
A2:
( p is AllSymbolsOf S -valued & SubWffsOf phi = [phi1,p] & phi = (<*((S -firstChar) . phi)*> ^ phi1) ^ p )
by Def34;
hereby ( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi implies phi = (<*x*> ^ phi2) ^ p2 )
assume A4:
phi = (<*x*> ^ phi2) ^ p2
;
( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi )then A5:
phi . 1 =
(<*x*> ^ (phi2 ^ p2)) . 1
by FINSEQ_1:32
.=
x
by FINSEQ_1:41
;
hence
x = (S -firstChar) . phi
by FOMODEL0:6;
( phi2 = head phi & p2 = tail phi )
(
rng p2 c= rng phi &
rng phi c= AllSymbolsOf S )
by A4, FINSEQ_1:30, RELAT_1:def 19;
then
(
p2 is
AllSymbolsOf S -valued &
[phi2,p2] = [phi2,p2] &
phi = (<*((S -firstChar) . phi)*> ^ phi2) ^ p2 )
by XBOOLE_1:1, RELAT_1:def 19, A5, FOMODEL0:6, A4;
then
SubWffsOf phi = [phi2,p2]
by A1, Def34;
hence
(
phi2 = head phi &
p2 = tail phi )
;
verum
end;
assume
( x = (S -firstChar) . phi & phi2 = head phi & p2 = tail phi )
; phi = (<*x*> ^ phi2) ^ p2
hence
phi = (<*x*> ^ phi2) ^ p2
by A2; verum