let Al be QC-alphabet ; :: thesis: 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; :: thesis: seq ((len g),(len f)) c= dom (g ^ f)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in seq ((len g),(len f)) or a in dom (g ^ f) )
assume A1: a in seq ((len g),(len f)) ; :: thesis: 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; :: thesis: verum