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 A1, A2, A3, CALCUL_1:def 1
.= Ant g by A1, A2, A3, CALCUL_1:def 1 ; :: thesis: Suc f = Suc g
Suc f = g . (len g) by A1, A2, CALCUL_1:def 2
.= Suc g by A1, A2, CALCUL_1:def 2 ;
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 A4, CALCUL_1:def 1
.= Ant g by A1, A4, CALCUL_1:def 1 ; :: thesis: Suc f = Suc g
thus Suc f = VERUM Al2 by A4, CALCUL_1:def 2
.= VERUM Al
.= Suc g by A1, A4, CALCUL_1:def 2 ; :: thesis: verum

end;

end;