let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for S being SigmaField of X
for M being sigma_Measure of S st f is bijective holds
ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )
let f be Function of X,Y; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S st f is bijective holds
ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S st f is bijective holds
ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )
let M be sigma_Measure of S; :: thesis: ( f is bijective implies ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) ) )
assume A1: f is bijective ; :: thesis: ex M1 being sigma_Measure of (CopyField (f,S)) st
( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )
reconsider S0 = S as Field_Subset of X ;
reconsider M0 = M as Measure of S0 ;
consider F being Function of (CopyField (f,S0)),S0 such that
A2: ( F = ((.: f) | S0) " & rng F = S0 & dom F = CopyField (f,S0) & F is bijective ) by A1, Th4;
consider G being Function of S0,(CopyField (f,S0)) such that
A3: ( G = (.: f) | S0 & dom G = S0 & rng G = CopyField (f,S0) & G is bijective ) by A1, Th4;
A4: CopyField (f,S0) = (.: f) .: S0 by A1, Def1;
then A5: CopyField (f,S0) = CopyField (f,S) by A1, Def2;
then reconsider F = F as Function of (CopyField (f,S)),S ;
reconsider G = G as Function of S,(CopyField (f,S)) by A1, A4, Def2;
consider M1 being Measure of (CopyField (f,S0)) such that
A6: ( M1 = M * (((.: f) | S0) ") & ( for s being Element of CopyField (f,S0) ex t being Element of S0 st
( s = f .: t & M1 . s = M . t ) ) ) by Th5, A1;
reconsider M1 = M1 as Measure of (CopyField (f,S)) by A5;
for s being Sep_Sequence of (CopyField (f,S)) holds SUM (M1 * s) = M1 . (union (rng s))

proof

let s be Sep_Sequence of (CopyField (f,S)); :: thesis: SUM (M1 * s) = M1 . (union (rng s))
defpred S₁[ Nat, set ] means ( s . $1 = f .: $2 & M1 . (s . $1) = M . $2 );
A7: for x being Element of NAT ex y being Element of S st S₁[x,y] by A5, A6;
consider t being Function of NAT,S such that
A8: for n being Element of NAT holds S₁[n,t . n] from FUNCT_2:sch 3(A7);
reconsider t = t as sequence of S ;
for m, n being object st m <> n holds
t . m misses t . n

proof

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

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

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

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

end;

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

then reconsider m1 = m, n1 = n as Element of NAT ;
A10: ( s . n1 = f .: (t . n1) & M1 . (s . n1) = M . (t . n1) ) by A8;
A11: ( s . m1 = f .: (t . m1) & M1 . (s . m1) = M . (t . m1) ) by A8;
s is disjoint_valued ;
then A12: s . m misses s . n by A9;

now :: thesis: not (t . m1) /\ (t . n1) <> {}

assume (t . m1) /\ (t . n1) <> {} ; :: thesis: contradiction
then consider x being object such that
A13: x in (t . m1) /\ (t . n1) by XBOOLE_0:def 1;
A14: x in t . m1 by XBOOLE_0:def 4, A13;
t . m1 in S ;
then t . m1 c= X ;
then t . m1 c= dom f by FUNCT_2:def 1;
then f . x in f .: ((t . m1) /\ (t . n1)) by A13, A14, FUNCT_1:def 6;
hence contradiction by A1, A10, A11, A12, FUNCT_1:62; :: thesis: verum

end;

hence t . m misses t . n ; :: thesis: verum

end;

end;

end;

then t is disjoint_valued ;
then reconsider t = t as Sep_Sequence of S ;
A15: ( dom s = NAT & dom t = NAT ) by FUNCT_2:def 1;
for n being Element of NAT holds (M1 * s) . n = (M * t) . n

proof

let n be Element of NAT ; :: thesis: (M1 * s) . n = (M * t) . n
A16: ( s . n = f .: (t . n) & M1 . (s . n) = M . (t . n) ) by A8;
(M1 * s) . n = M1 . (s . n) by A15, FUNCT_1:13;
hence (M1 * s) . n = (M * t) . n by A16, A15, FUNCT_1:13; :: thesis: verum

end;

then A17: M1 * s = M * t by FUNCT_2:63;
for z being object holds
( z in union (rng s) iff z in f .: (union (rng t)) )

proof

let z be object ; :: thesis: ( z in union (rng s) iff z in f .: (union (rng t)) )

hereby :: thesis: ( z in f .: (union (rng t)) implies z in union (rng s) )

assume z in union (rng s) ; :: thesis: z in f .: (union (rng t))
then consider Y being set such that
A18: ( z in Y & Y in rng s ) by TARSKI:def 4;
consider n being Element of NAT such that
A19: ( n in dom s & Y = s . n ) by A18, PARTFUN1:3;
A20: z in f .: (t . n) by A8, A18, A19;
t . n in rng t by A15, FUNCT_1:def 3;
then f .: (t . n) c= f .: (union (rng t)) by RELAT_1:123, ZFMISC_1:74;
hence z in f .: (union (rng t)) by A20; :: thesis: verum

end;

assume z in f .: (union (rng t)) ; :: thesis: z in union (rng s)
then consider x being object such that
A21: ( x in dom f & x in union (rng t) & z = f . x ) by FUNCT_1:def 6;
consider Y being set such that
A22: ( x in Y & Y in rng t ) by A21, TARSKI:def 4;
consider n being Element of NAT such that
A23: ( n in dom t & Y = t . n ) by A22, PARTFUN1:3;
z in f .: (t . n) by A21, A22, A23, FUNCT_1:def 6;
then A24: z in s . n by A8;
s . n in rng s by A15, FUNCT_1:3;
hence z in union (rng s) by A24, TARSKI:def 4; :: thesis: verum

end;

then A25: union (rng s) = f .: (union (rng t)) by TARSKI:2;
F * G = id (dom G) by A2, A3, FUNCT_1:39;
then A26: F * G = id (dom M) by A3, FUNCT_2:def 1;
M1 * G = M * (F * G) by A2, A6, RELAT_1:36;
then M1 * G = M by A26, RELAT_1:52;
then M . (union (rng t)) = M1 . (G . (union (rng t))) by A3, FUNCT_1:13;
then M . (union (rng t)) = M1 . ((.: f) . (union (rng t))) by A3, FUNCT_1:49;
then M . (union (rng t)) = M1 . (union (rng s)) by A1, A25, Th1;
hence SUM (M1 * s) = M1 . (union (rng s)) by A17, MEASURE1:def 6; :: thesis: verum

end;

then reconsider M1 = M1 as sigma_Measure of (CopyField (f,S)) by MEASURE1:def 6;
take M1 ; :: thesis: ( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) )
thus ( M1 = M * (((.: f) | S) ") & ( for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t ) ) ) by A5, A6; :: thesis: verum