let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for f being FinSequence of CQC-WFF Al2
for g being FinSequence of CQC-WFF Al st f = g holds
( Ant f = Ant g & Suc f = Suc g )

let Al2 be Al -expanding QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al2
for g being FinSequence of CQC-WFF Al st f = g holds
( Ant f = Ant g & Suc f = Suc g )

let f be FinSequence of CQC-WFF Al2; :: thesis: for g being FinSequence of CQC-WFF Al st f = g holds
( Ant f = Ant g & Suc f = Suc g )

let g be FinSequence of CQC-WFF Al; :: thesis: ( f = g implies ( Ant f = Ant g & Suc f = Suc g ) )
assume A1: f = g ; :: thesis: ( Ant f = Ant g & Suc f = Suc g )
per cases ( len f > 0 or not len f > 0 ) ;
suppose A2: len f > 0 ; :: thesis: ( Ant f = Ant g & Suc f = Suc g )
then consider k being Nat such that
A3: len f = k + 1 by NAT_1:6;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
thus Ant f = g | (Seg k) by
.= Ant g by ; :: thesis: Suc f = Suc g
Suc f = g . (len g) by
.= Suc g by ;
hence Suc f = Suc g ; :: thesis: verum
end;
suppose A4: not len f > 0 ; :: thesis: ( Ant f = Ant g & Suc f = Suc g )
thus Ant f = {} by
.= Ant g by ; :: thesis: Suc f = Suc g
thus Suc f = VERUM Al2 by
.= VERUM Al
.= Suc g by ; :: thesis: verum
end;
end;