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

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