let X be non empty set ; :: thesis: for f being FinSequence of X holds PairF f is FinSequence of the carrier' of ()
let f be FinSequence of X; :: thesis: PairF f is FinSequence of the carrier' of ()
rng () c= [:X,X:]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng () or y in [:X,X:] )
A1: (len f) -' 1 < ((len f) -' 1) + 1 by NAT_1:13;
assume y in rng () ; :: thesis: y in [:X,X:]
then consider x being object such that
A2: x in dom () and
A3: y = () . x by FUNCT_1:def 3;
reconsider n = x as Element of NAT by A2;
A4: x in Seg (len ()) by ;
then A5: 1 <= n by FINSEQ_1:1;
A6: len () = (len f) -' 1 by Def2;
A7: n <= len () by ;
then 1 <= (len f) -' 1 by ;
then (len f) -' 1 = (len f) - 1 by NAT_D:39;
then A8: n < len f by ;
then A9: n + 1 <= len f by NAT_1:13;
1 < n + 1 by ;
then n + 1 in dom f by ;
then A10: f . (n + 1) in rng f by FUNCT_1:def 3;
n in dom f by ;
then A11: f . n in rng f by FUNCT_1:def 3;
(PairF f) . n = [(f . n),(f . (n + 1))] by A5, A8, Def2;
hence y in [:X,X:] by ; :: thesis: verum
end;
hence PairF f is FinSequence of the carrier' of () by FINSEQ_1:def 4; :: thesis: verum