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 )

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

end;

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

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;.= 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