let g, f be FinSequence of CQC-WFF ; :: thesis: seq ((len g),(len f)) c= dom (g ^ f)

now

let a be set ; :: thesis: ( a in seq ((len g),(len f)) implies 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

end;

hence seq ((len g),(len f)) c= dom (g ^ f) by TARSKI:def 3; :: thesis: verum