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;
A2: ( 1 + (len g) <= n & n <= (len f) + (len g) ) by A1, Th1;
1 <= 1 + (len g) by NAT_1:11;
then ( 1 <= n & n <= len (g ^ f) ) by A2, FINSEQ_1:35, XXREAL_0:2;
hence a in dom (g ^ f) by FINSEQ_3:27; :: thesis: verum

end;

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