let X, Y be non empty set ; :: thesis: for S being SigmaField of X
for T being Function of X,Y
for F being Finite_Sep_Sequence of S st T is bijective holds
((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)
let S be SigmaField of X; :: thesis: for T being Function of X,Y
for F being Finite_Sep_Sequence of S st T is bijective holds
((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)
let T be Function of X,Y; :: thesis: for F being Finite_Sep_Sequence of S st T is bijective holds
((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)
let F be Finite_Sep_Sequence of S; :: thesis: ( T is bijective implies ((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S) )
assume A1: T is bijective ; :: thesis: ((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S)
set H = (.: T) | S;
rng ((.: T) | S) = (.: T) .: S by RELAT_1:115;
then A2: rng ((.: T) | S) = CopyField (T,S) by A1, Def2;
dom ((.: T) | S) = S by FUNCT_2:def 1;
then reconsider H = (.: T) | S as Function of S,(CopyField (T,S)) by A2, FUNCT_2:1;
reconsider G = H * F as FinSequence of CopyField (T,S) ;
for m, n being object st m <> n holds
G . m misses G . n

proof

let m, n be object ; :: thesis: ( m <> n implies G . m misses G . n )
assume A3: m <> n ; :: thesis: G . m misses G . n

per cases ( not m in dom G or not n in dom G or ( m in dom G & n in dom G ) ) ;

suppose ( not m in dom G or not n in dom G ) ; :: thesis: G . m misses G . n

then ( G . m = {} or G . n = {} ) by FUNCT_1:def 2;
hence G . m misses G . n ; :: thesis: verum

end;

suppose A4: ( m in dom G & n in dom G ) ; :: thesis: G . m misses G . n

then reconsider m1 = m, n1 = n as Element of NAT ;
G . n1 = H . (F . n1) by A4, FUNCT_1:12;
then G . n1 = (.: T) . (F . n1) by FUNCT_1:49;
then A5: G . n1 = T .: (F . n1) by A1, Th1;
G . m1 = H . (F . m1) by A4, FUNCT_1:12;
then G . m1 = (.: T) . (F . m1) by FUNCT_1:49;
then A6: G . m1 = T .: (F . m1) by A1, Th1;
F is disjoint_valued ;
then F . m misses F . n by A3;
then {} = T .: ((F . m1) /\ (F . n1)) ;
hence G . m misses G . n by A1, A5, A6, FUNCT_1:62; :: thesis: verum

end;

end;

end;

then G is disjoint_valued ;
hence ((.: T) | S) * F is Finite_Sep_Sequence of CopyField (T,S) ; :: thesis: verum