let Al be QC-alphabet ; for f, g being FinSequence of CQC-WFF Al holds seq ((len g),(len f)) c= dom (g ^ f)
let f, g be FinSequence of CQC-WFF Al; seq ((len g),(len f)) c= dom (g ^ f)
let a be object ; TARSKI:def 3 ( not a in seq ((len g),(len f)) or a in dom (g ^ f) )
assume A1:
a in seq ((len g),(len f))
; a in dom (g ^ f)
reconsider n = a as Element of NAT by A1;
n <= (len f) + (len g)
by A1, Th1;
then A2:
n <= len (g ^ f)
by FINSEQ_1:22;
A3:
1 <= 1 + (len g)
by NAT_1:11;
1 + (len g) <= n
by A1, Th1;
then
1 <= n
by A3, XXREAL_0:2;
hence
a in dom (g ^ f)
by A2, FINSEQ_3:25; verum