:: CALCUL_2 semantic presentation

definition
let c1, c2 be natural number ;
func seq c1,c2 -> set equals :: CALCUL_2:def 1
{ b1 where B is Nat : ( 1 + a1 <= b1 & b1 <= a2 + a1 ) } ;
coherence
{ b1 where B is Nat : ( 1 + c1 <= b1 & b1 <= c2 + c1 ) } is set ;
end;

:: deftheorem Def1 defines seq CALCUL_2:def 1 :
for b1, b2 being natural number holds seq b1,b2 = { b3 where B is Nat : ( 1 + b1 <= b3 & b3 <= b2 + b1 ) } ;

definition
let c1, c2 be natural number ;
redefine func seq as seq c1,c2 -> Subset of NAT ;
coherence
seq c1,c2 is Subset of NAT
proof
set c3 = seq c1,c2;
seq c1,c2 c= NAT
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in seq c1,c2 ;
then c4 in { b1 where B is Nat : ( 1 + c1 <= b1 & b1 <= c2 + c1 ) } ;
then ex b1 being Nat st
( c4 = b1 & 1 + c1 <= b1 & b1 <= c2 + c1 ) ;
hence c4 in NAT ;
end;
hence seq c1,c2 is Subset of NAT ;
end;
end;

theorem Th1: :: CALCUL_2:1
for b1, b2, b3 being natural number holds
( b1 in seq b2,b3 iff ( 1 + b2 <= b1 & b1 <= b3 + b2 ) )
proof
let c1, c2, c3 be natural number ;
E2: c1 is Nat by ORDINAL1:def 13;
( c1 in { b1 where B is Nat : ( 1 + c2 <= b1 & b1 <= c3 + c2 ) } iff ex b1 being Nat st
( c1 = b1 & 1 + c2 <= b1 & b1 <= c3 + c2 ) ) ;
hence ( c1 in seq c2,c3 iff ( 1 + c2 <= c1 & c1 <= c3 + c2 ) ) by E2;
end;

theorem Th2: :: CALCUL_2:2
for b1 being natural number holds seq b1,0 = {}
proof
let c1 be natural number ;
hereby
consider c2 being Element of seq c1,0;
assume E3: seq c1,0 <> {} ;
then reconsider c3 = c2 as Nat by TARSKI:def 3;
( 1 + c1 <= c3 & c3 <= 0 + c1 ) by E3, Th1;
hence not verum by NAT_1:38;
end;
end;

theorem Th3: :: CALCUL_2:3
for b1, b2 being natural number holds
( b1 = 0 or b1 + b2 in seq b2,b1 )
proof
let c1, c2 be natural number ;
assume c1 <> 0 ;
then consider c3 being Nat such that
E4: c1 = c3 + 1 by NAT_1:22;
E5: c1 + c2 is Nat by ORDINAL1:def 13;
1 <= c1 by E4, NAT_1:29;
then ( 1 + c2 <= c1 + c2 & c1 + c2 <= c1 + c2 ) by XREAL_1:8;
then c1 + c2 in { b1 where B is Nat : ( 1 + c2 <= b1 & b1 <= c1 + c2 ) } by E5;
hence c1 + c2 in seq c2,c1 ;
end;

theorem Th4: :: CALCUL_2:4
for b1, b2, b3 being natural number holds
( b1 <= b2 iff seq b3,b1 c= seq b3,b2 )
proof
let c1, c2, c3 be natural number ;
thus ( c1 <= c2 implies seq c3,c1 c= seq c3,c2 )
proof
assume E5: c1 <= c2 ;
let c4 be set ; :: according to TARSKI:def 3
assume E6: c4 in seq c3,c1 ;
reconsider c5 = c4 as Nat by E6;
E7: ( 1 + c3 <= c5 & c5 <= c1 + c3 ) by E6, Th1;
c1 + c3 <= c2 + c3 by E5, XREAL_1:8;
then c5 <= c2 + c3 by E7, XXREAL_0:2;
then c4 in { b1 where B is Nat : ( 1 + c3 <= b1 & b1 <= c2 + c3 ) } by E7;
hence c4 in seq c3,c2 ;
end;
assume E5: seq c3,c1 c= seq c3,c2 ;
now
assume c1 <> 0 ;
then c1 + c3 in seq c3,c1 by Th3;
then c1 + c3 <= c2 + c3 by E5, Th1;
hence c1 <= c2 by XREAL_1:8;
end;
hence c1 <= c2 ;
end;

theorem Th5: :: CALCUL_2:5
for b1, b2 being natural number holds (seq b1,b2) \/ {((b1 + b2) + 1)} = seq b1,(b2 + 1)
proof
let c1, c2 be natural number ;
thus (seq c1,c2) \/ {((c1 + c2) + 1)} c= seq c1,(c2 + 1) :: according to XBOOLE_0:def 10
proof
c2 + 0 <= c2 + 1 by XREAL_1:9;
then E6: seq c1,c2 c= seq c1,(c2 + 1) by Th4;
let c3 be set ; :: according to TARSKI:def 3
assume E7: c3 in (seq c1,c2) \/ {((c1 + c2) + 1)} ;
( c3 in seq c1,c2 or c3 in {((c1 + c2) + 1)} ) by E7, XBOOLE_0:def 2;
then ( c3 in seq c1,(c2 + 1) or c3 = c1 + (c2 + 1) ) by E6, TARSKI:def 1;
hence c3 in seq c1,(c2 + 1) by Th3;
end;
let c3 be set ; :: according to TARSKI:def 3
assume E6: c3 in seq c1,(c2 + 1) ;
reconsider c4 = c3 as Nat by E6;
( 1 + c1 <= c4 & c4 <= (c2 + 1) + c1 ) by E6, Th1;
then ( 1 + c1 <= c4 & ( c4 <= c1 + c2 or c4 = (c1 + c2) + 1 ) ) by NAT_1:26;
then ( c4 in seq c1,c2 or c4 in {((c1 + c2) + 1)} ) by TARSKI:def 1;
hence c3 in (seq c1,c2) \/ {((c1 + c2) + 1)} by XBOOLE_0:def 2;
end;

theorem Th6: :: CALCUL_2:6
for b1, b2 being Nat holds seq b1,b2,b2 are_equipotent
proof
let c1, c2 be Nat;
defpred S1[ Nat] means seq c1,a1,a1 are_equipotent ;
E7: S1[0] by Th2;
E8: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c3 be Nat;
assume E9: seq c1,c3,c3 are_equipotent ;
reconsider c4 = c1 + c3 as Nat ;
E10: seq c1,(c3 + 1) = (seq c1,c3) \/ {(c4 + 1)} by Th5;
E11: c3 + 1 = succ c3 by CARD_1:52
.= c3 \/ {c3} by ORDINAL1:def 1 ;
E12: {(c4 + 1)},{c3} are_equipotent by CARD_1:48;
E13: now
assume c3 meets {c3} ;
then consider c5 being set such that
E14: ( c5 in c3 & c5 in {c3} ) by XBOOLE_0:3;
c5 = c3 by E14, TARSKI:def 1;
hence not verum by E14;
end;
now
assume seq c1,c3 meets {(c4 + 1)} ;
then consider c5 being set such that
E14: ( c5 in seq c1,c3 & c5 in {(c4 + 1)} ) by XBOOLE_0:3;
E15: ( c5 = c4 + 1 & c3 + c1 <= c4 ) by E14, TARSKI:def 1;
not c4 + 1 <= c4 by NAT_1:38;
hence not verum by E14, E15, Th1;
end;
hence S1[c3 + 1] by E9, E10, E11, E12, E13, CARD_1:58;
end;
for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E7, E8);
 hence seq c1,c2,c2 are_equipotent ;
end;

registration
let c1, c2 be Nat;
cluster seq a1,a2 -> finite ;
coherence
seq c1,c2 is finite
proof
E7: c2 is finite by CARD_1:69;
c2, seq c1,c2 are_equipotent by Th6;
hence seq c1,c2 is finite by E7, CARD_1:68;
end;
end;

registration
let c1 be FinSequence of CQC-WFF ;
cluster Card a1 -> finite ;
coherence
len c1 is finite by CARD_1:69;
end;

theorem Th7: :: CALCUL_2:7
for b1, b2 being Nat holds seq b1,b2 c= Seg (b1 + b2)
proof
let c1, c2 be Nat;
let c3 be set ; :: according to TARSKI:def 3
assume E8: c3 in seq c1,c2 ;
then reconsider c4 = c3 as Nat ;
E9: ( 1 + c1 <= c4 & c4 <= c2 + c1 ) by E8, Th1;
1 <= 1 + c1 by NAT_1:29;
then 1 <= c4 by E9, XXREAL_0:2;
hence c3 in Seg (c1 + c2) by E9, FINSEQ_1:3;
end;

theorem Th8: :: CALCUL_2:8
for b1, b2 being Nat holds Seg b1 misses seq b1,b2
proof
let c1, c2 be Nat;
assume Seg c1 meets seq c1,c2 ;
then consider c3 being set such that
E8: ( c3 in Seg c1 & c3 in seq c1,c2 ) by XBOOLE_0:3;
reconsider c4 = c3 as Nat by E8;
( c4 <= c1 & c1 + 1 <= c4 ) by E8, Th1, FINSEQ_1:3;
hence not verum by NAT_1:38;
end;

theorem Th9: :: CALCUL_2:9
for b1, b2 being FinSequence holds Seg (len (b1 ^ b2)) = (Seg (len b1)) \/ (seq (len b1),(len b2))
proof
let c1, c2 be FinSequence;
now
let c3 be set ;
assume E8: c3 in Seg (len (c1 ^ c2)) ;
reconsider c4 = c3 as Nat by E8;
E9: ( 1 <= c4 & c4 <= len (c1 ^ c2) ) by E8, FINSEQ_1:3;
E10: now
assume c4 <= len c1 ;
then E11: c4 in Seg (len c1) by E9, FINSEQ_1:3;
Seg (len c1) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by XBOOLE_1:7;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E11;
end;
now
assume len c1 < c4 ;
then ( (len c1) + 1 <= c4 & c4 <= (len c1) + (len c2) ) by E9, FINSEQ_1:35, NAT_1:38;
then E11: c3 in seq (len c1),(len c2) ;
seq (len c1),(len c2) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by XBOOLE_1:7;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E11;
end;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E10;
end;
hence Seg (len (c1 ^ c2)) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by TARSKI:def 3; :: according to XBOOLE_0:def 10
let c3 be set ; :: according to TARSKI:def 3
assume E8: c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) ;
E9: now
assume E10: c3 in Seg (len c1) ;
then reconsider c4 = c3 as Nat ;
E11: ( 1 <= c4 & c4 <= len c1 ) by E10, FINSEQ_1:3;
len c1 <= len (c1 ^ c2) by CALCUL_1:6;
then c4 <= len (c1 ^ c2) by E11, XXREAL_0:2;
hence c3 in Seg (len (c1 ^ c2)) by E11, FINSEQ_1:3;
end;
now
assume E10: c3 in seq (len c1),(len c2) ;
then reconsider c4 = c3 as Nat ;
E11: ( 1 + (len c1) <= c4 & c4 <= (len c2) + (len c1) ) by E10, Th1;
then E12: c4 <= len (c1 ^ c2) by FINSEQ_1:35;
1 <= 1 + (len c1) by NAT_1:29;
then 1 <= c4 by E11, XXREAL_0:2;
hence c3 in Seg (len (c1 ^ c2)) by E12, FINSEQ_1:3;
end;
hence c3 in Seg (len (c1 ^ c2)) by E8, E9, XBOOLE_0:def 2;
end;

theorem Th10: :: CALCUL_2:10
for b1, b2 being FinSequence of CQC-WFF holds len (Sgm (seq (len b1),(len b2))) = len b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
seq (len c1),(len c2), len c2 are_equipotent by Th6;
then card (seq (len c1),(len c2)) = card (len c2) by CARD_1:81;
then E9: card (seq (len c1),(len c2)) = len c2 by FINSEQ_1:78;
seq (len c1),(len c2) c= Seg ((len c1) + (len c2)) by Th7;
hence len (Sgm (seq (len c1),(len c2))) = len c2 by E9, FINSEQ_3:44;
end;

theorem Th11: :: CALCUL_2:11
for b1, b2 being FinSequence of CQC-WFF holds dom (Sgm (seq (len b1),(len b2))) = dom b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
len (Sgm (seq (len c1),(len c2))) = len c2 by Th10;
hence dom (Sgm (seq (len c1),(len c2))) = dom c2 by FINSEQ_3:31;
end;

theorem Th12: :: CALCUL_2:12
for b1, b2 being FinSequence of CQC-WFF holds rng (Sgm (seq (len b1),(len b2))) = seq (len b1),(len b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
seq (len c1),(len c2) c= Seg ((len c1) + (len c2)) by Th7;
hence rng (Sgm (seq (len c1),(len c2))) = seq (len c1),(len c2) by FINSEQ_1:def 13;
end;

theorem Th13: :: CALCUL_2:13
for b1 being Nat
for b2, b3 being FinSequence of CQC-WFF holds
( b1 in dom (Sgm (seq (len b2),(len b3))) implies (Sgm (seq (len b2),(len b3))) . b1 = (len b2) + b1 )
proof
let c1 be Nat;
let c2, c3 be FinSequence of CQC-WFF ;
assume c1 in dom (Sgm (seq (len c2),(len c3))) ;
then c1 in dom c3 by Th11;
then E12: ( 1 <= c1 & c1 <= len c3 ) by FINSEQ_3:27;
defpred S1[ Nat] means ( 1 <= a1 & a1 <= len c3 implies for b1 being Nat holds
( 1 <= b1 & b1 <= a1 implies (Sgm (seq (len c2),(len c3))) . b1 = (len c2) + b1 ) );
E13: S1[0] ;
E14: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c4 be Nat;
assume E15: S1[c4] ;
assume E16: ( 1 <= c4 + 1 & c4 + 1 <= len c3 ) ;
let c5 be Nat;
assume E17: ( 1 <= c5 & c5 <= c4 + 1 ) ;
E18: ( c5 <= c4 implies (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 ) by E15, E16, E17, XXREAL_0:2, NAT_1:38;
now
assume E19: c5 = c4 + 1 ;
dom (Sgm (seq (len c2),(len c3))) = dom c3 by Th11;
then c5 in dom (Sgm (seq (len c2),(len c3))) by E16, E19, FINSEQ_3:27;
then (Sgm (seq (len c2),(len c3))) . c5 in rng (Sgm (seq (len c2),(len c3))) by FUNCT_1:12;
then reconsider c6 = (Sgm (seq (len c2),(len c3))) . c5 as Nat ;
E20: now
assume E21: c6 < (len c2) + (c4 + 1) ;
E22: now
assume E23: c4 = 0 ;
then not c6 in seq (len c2),(len c3) by E21, Th1;
then E24: not c6 in rng (Sgm (seq (len c2),(len c3))) by Th12;
1 <= len c3 by E16, XXREAL_0:2;
then 1 in dom c3 by FINSEQ_3:27;
then 1 in dom (Sgm (seq (len c2),(len c3))) by Th11;
hence not verum by E19, E23, E24, FUNCT_1:12;
end;
now
assume E23: c4 <> 0 ;
E24: c6 < ((len c2) + c4) + 1 by E21;
0 < c4 by E23;
then E25: ( 0 + 1 <= c4 & c4 <= c4 + 1 ) by NAT_1:38;
E26: (Sgm (seq (len c2),(len c3))) . c4 = (len c2) + c4 by E15, E16, E25, XXREAL_0:2;
then reconsider c7 = (Sgm (seq (len c2),(len c3))) . c4 as Nat ;
E27: ( 1 <= c4 & c4 < c4 + 1 & c4 + 1 <= len (Sgm (seq (len c2),(len c3))) ) by E16, E25, Th10, NAT_1:38;
( c6 <= c7 & seq (len c2),(len c3) c= Seg ((len c2) + (len c3)) ) by E24, E26, Th7, NAT_1:38;
hence not verum by E19, E27, FINSEQ_1:def 13;
end;
hence not verum by E22;
end;
now
assume E21: c6 > (len c2) + (c4 + 1) ;
E22: 1 + (len c2) <= (1 + (len c2)) + c4 by NAT_1:29;
(len c2) + (c4 + 1) <= (len c3) + (len c2) by E16, XREAL_1:8;
then (len c2) + (c4 + 1) in seq (len c2),(len c3) by E22;
then (len c2) + (c4 + 1) in rng (Sgm (seq (len c2),(len c3))) by Th12;
then consider c7 being Nat such that
E23: ( c7 in dom (Sgm (seq (len c2),(len c3))) & (Sgm (seq (len c2),(len c3))) . c7 = (len c2) + (c4 + 1) ) by FINSEQ_2:11;
E24: now
assume E25: c7 <= c4 + 1 ;
now
assume E26: c7 <= c4 ;
then E27: c7 < c4 + 1 by NAT_1:38;
now
assume 1 <= c7 ;
then (len c2) + (c4 + 1) = (len c2) + c7 by E15, E16, E23, E26, XXREAL_0:2, NAT_1:38;
hence not verum by E27;
end;
hence not verum by E23, FINSEQ_3:27;
end;
hence not verum by E19, E21, E23, E25, NAT_1:26;
end;
reconsider c8 = (Sgm (seq (len c2),(len c3))) . c7 as Nat by E23;
E25: ( 1 <= c5 & c5 < c7 & c7 <= len (Sgm (seq (len c2),(len c3))) ) by E19, E23, E24, FINSEQ_3:27, NAT_1:29;
seq (len c2),(len c3) c= Seg ((len c2) + (len c3)) by Th7;
hence not verum by E21, E23, E25, FINSEQ_1:def 13;
end;
hence (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 by E19, E20, XXREAL_0:1;
end;
hence (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 by E17, E18, NAT_1:26;
end;
for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E13, E14);
 hence (Sgm (seq (len c2),(len c3))) . c1 = (len c2) + c1 by E12;
end;

theorem Th14: :: CALCUL_2:14
for b1, b2 being FinSequence of CQC-WFF holds seq (len b1),(len b2) c= dom (b1 ^ b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
now
let c3 be set ;
assume E13: c3 in seq (len c1),(len c2) ;
reconsider c4 = c3 as Nat by E13;
E14: ( 1 + (len c1) <= c4 & c4 <= (len c2) + (len c1) ) by E13, Th1;
1 <= 1 + (len c1) by NAT_1:29;
then ( 1 <= c4 & c4 <= len (c1 ^ c2) ) by E14, XXREAL_0:2, FINSEQ_1:35;
hence c3 in dom (c1 ^ c2) by FINSEQ_3:27;
end;
hence seq (len c1),(len c2) c= dom (c1 ^ c2) by TARSKI:def 3;
end;

theorem Th15: :: CALCUL_2:15
for b1, b2 being FinSequence of CQC-WFF holds dom ((b1 ^ b2) | (seq (len b1),(len b2))) = seq (len b1),(len b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
E14: dom ((c1 ^ c2) | (seq (len c1),(len c2))) = (dom (c1 ^ c2)) /\ (seq (len c1),(len c2)) by RELAT_1:90;
seq (len c1),(len c2) c= dom (c1 ^ c2) by Th14;
hence dom ((c1 ^ c2) | (seq (len c1),(len c2))) = seq (len c1),(len c2) by E14, XBOOLE_1:28;
end;

theorem Th16: :: CALCUL_2:16
for b1, b2 being FinSequence of CQC-WFF holds Seq ((b1 ^ b2) | (seq (len b1),(len b2))) = (Sgm (seq (len b1),(len b2))) * (b1 ^ b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
reconsider c3 = (c1 ^ c2) | (seq (len c1),(len c2)) as FinSubsequence ;
Seq c3 = c3 * (Sgm (dom c3)) by FINSEQ_1:def 14
.= c3 * (Sgm (seq (len c1),(len c2))) by Th15
.= ((c1 ^ c2) | (rng (Sgm (seq (len c1),(len c2))))) * (Sgm (seq (len c1),(len c2))) by Th12
.= (c1 ^ c2) * (Sgm (seq (len c1),(len c2))) by FUNCT_4:2 ;
hence Seq ((c1 ^ c2) | (seq (len c1),(len c2))) = (Sgm (seq (len c1),(len c2))) * (c1 ^ c2) ;
end;

theorem Th17: :: CALCUL_2:17
for b1, b2 being FinSequence of CQC-WFF holds dom (Seq ((b1 ^ b2) | (seq (len b1),(len b2)))) = dom b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
rng (Sgm (seq (len c1),(len c2))) = seq (len c1),(len c2) by Th12;
then E16: rng (Sgm (seq (len c1),(len c2))) c= dom (c1 ^ c2) by Th14;
dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom ((Sgm (seq (len c1),(len c2))) * (c1 ^ c2)) by Th16;
then dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom (Sgm (seq (len c1),(len c2))) by E16, RELAT_1:46;
hence dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom c2 by Th11;
end;

theorem Th18: :: CALCUL_2:18
for b1, b2 being FinSequence of CQC-WFF holds b1 is_Subsequence_of b2 ^ b1
proof
let c1, c2 be FinSequence of CQC-WFF ;
E17: for b1 being Nat holds
( b1 in dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) implies (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . b1 = c1 . b1 )
proof
let c3 be Nat;
assume E18: c3 in dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) ;
E19: (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = ((Sgm (seq (len c2),(len c1))) * (c2 ^ c1)) . c3 by Th16;
E20: c3 in dom c1 by E18, Th17;
then E21: c3 in dom (Sgm (seq (len c2),(len c1))) by Th11;
then (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = (c2 ^ c1) . ((Sgm (seq (len c2),(len c1))) . c3) by E19, FUNCT_1:23;
then (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = (c2 ^ c1) . ((len c2) + c3) by E21, Th13;
hence (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = c1 . c3 by E20, FINSEQ_1:def 7;
end;
dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) = dom c1 by Th17;
then Seq ((c2 ^ c1) | (seq (len c2),(len c1))) = c1 by E17, FINSEQ_1:17;
hence c1 is_Subsequence_of c2 ^ c1 by CALCUL_1:def 4;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be Permutation of dom c2;
func Per c2,c3 -> FinSequence of a1 equals :: CALCUL_2:def 2
a3 * a2;
coherence
c3 * c2 is FinSequence of c1
proof
c3 is onto by FUNCT_2:def 4;
then E17: rng c3 = dom c2 by FUNCT_2:def 3;
then dom (c3 * c2) = dom c3 by RELAT_1:46;
then dom (c3 * c2) = dom c2 by FUNCT_2:67;
then consider c4 being Nat such that
E18: dom (c3 * c2) = Seg c4 by FINSEQ_1:def 2;
reconsider c5 = c3 * c2 as FinSequence by E18, FINSEQ_1:def 2;
rng c5 = rng c