let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for S being Field_Subset of X
for M being Measure of S st f is bijective holds
ex M1 being 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 Field_Subset of X
for M being Measure of S st f is bijective holds
ex M1 being 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 Field_Subset of X; :: thesis: for M being Measure of S st f is bijective holds
ex M1 being 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 Measure of S; :: thesis: ( f is bijective implies ex M1 being 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 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 ) ) )
then A2: CopyField (f,S) = (.: f) .: S by Def1;
consider F being Function of (CopyField (f,S)),S such that
A3: ( F = ((.: f) | S) " & rng F = S & dom F = CopyField (f,S) & F is bijective ) by A1, Th4;
consider G being Function of S,(CopyField (f,S)) such that
A4: ( G = (.: f) | S & dom G = S & rng G = CopyField (f,S) & G is bijective ) by A1, Th4;
reconsider M1 = M * F as Function of (CopyField (f,S)),ExtREAL ;
A5: {} c= X ;
A6: {} in dom G by A4, PROB_1:4;
((.: f) | S) . {} = (.: f) . {} by FUNCT_1:49, PROB_1:4;
then ((.: f) | S) . {} = f .: {} by A5, A1, Th1;
then A7: {} = F . {} by FUNCT_1:34, A3, A4, A6;
then M1 . {} = M . {} by A3, FUNCT_1:13, PROB_1:4;
then A8: M1 is zeroed by VALUED_0:def 19;
A9: for s being Element of CopyField (f,S) ex t being Element of S st
( s = f .: t & M1 . s = M . t )

proof

let s be Element of CopyField (f,S); :: thesis: ex t being Element of S st
( s = f .: t & M1 . s = M . t )
consider t being object such that
A10: ( t in dom (.: f) & t in S & s = (.: f) . t ) by A2, FUNCT_1:def 6;
reconsider t = t as Element of S by A10;
A11: s = G . t by A4, A10, FUNCT_1:49;
take t ; :: thesis: ( s = f .: t & M1 . s = M . t )
thus s = f .: t by A1, A10, Th1; :: thesis: M1 . s = M . t
M1 . s = M . (F . s) by A3, FUNCT_1:13;
hence M1 . s = M . t by A3, A4, A11, FUNCT_1:34; :: thesis: verum

end;

for A, B being Element of CopyField (f,S) st A misses B & A \/ B in CopyField (f,S) holds
M1 . (A \/ B) = (M1 . A) + (M1 . B)

proof

let A, B be Element of CopyField (f,S); :: thesis: ( A misses B & A \/ B in CopyField (f,S) implies M1 . (A \/ B) = (M1 . A) + (M1 . B) )
assume A12: ( A misses B & A \/ B in CopyField (f,S) ) ; :: thesis: M1 . (A \/ B) = (M1 . A) + (M1 . B)
consider a being Element of S such that
A13: ( A = f .: a & M1 . A = M . a ) by A9;
consider b being Element of S such that
A14: ( B = f .: b & M1 . B = M . b ) by A9;
A /\ B = f .: (a /\ b) by FUNCT_1:62, A1, A13, A14;
then A /\ B = (.: f) . (a /\ b) by A1, Th1;
then {} = G . (a /\ b) by A12, A4, FUNCT_1:49;
then A15: a misses b by A7, A3, A4, FUNCT_1:34;
A \/ B = f .: (a \/ b) by RELAT_1:120, A13, A14;
then A \/ B = (.: f) . (a \/ b) by A1, Th1;
then A \/ B = G . (a \/ b) by A4, FUNCT_1:49;
then M1 . (A \/ B) = M . (F . (G . (a \/ b))) by FUNCT_1:13, A3;
then M1 . (A \/ B) = M . (a \/ b) by A3, A4, FUNCT_1:34;
hence M1 . (A \/ B) = (M1 . A) + (M1 . B) by A13, A14, A15, MEASURE1:def 3; :: thesis: verum

end;

then M1 is additive ;
hence ex M1 being 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 ) ) ) by A3, A8, A9; :: thesis: verum