let X, Y be non empty set ; for S being SigmaField of X
for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S holds
g is_simple_func_in CopyField (T,S)
let S be SigmaField of X; for T being Function of X,Y
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S holds
g is_simple_func_in CopyField (T,S)
let T be Function of X,Y; for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S holds
g is_simple_func_in CopyField (T,S)
let f be PartFunc of X,ExtREAL; for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S holds
g is_simple_func_in CopyField (T,S)
let g be PartFunc of Y,ExtREAL; ( T is bijective & g = f * (T ") & f is_simple_func_in S implies g is_simple_func_in CopyField (T,S) )
assume that
A1:
T is bijective
and
A2:
g = f * (T ")
and
A3:
f is_simple_func_in S
; g is_simple_func_in CopyField (T,S)
f is real-valued
by A3, MESFUNC2:def 4;
then A4:
rng f c= REAL
;
A5:
( dom T = X & rng T = Y )
by A1, FUNCT_2:def 1, FUNCT_2:def 3;
A6:
( rng T = dom (T ") & dom T = rng (T ") )
by A1, FUNCT_1:33;
consider F being Finite_Sep_Sequence of S such that
A7:
( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) )
by A3, MESFUNC2:def 4;
rng g c= rng f
by A2, RELAT_1:26;
then
rng g c= REAL
by A4;
then A8:
g is real-valued
;
set H = (.: T) | S;
rng ((.: T) | S) = (.: T) .: S
by RELAT_1:115;
then A9:
rng ((.: T) | S) = CopyField (T,S)
by A1, Def2;
A10:
dom ((.: T) | S) = S
by FUNCT_2:def 1;
then reconsider H = (.: T) | S as Function of S,(CopyField (T,S)) by A9, FUNCT_2:1;
reconsider G = H * F as Finite_Sep_Sequence of CopyField (T,S) by Th21, A1;
A11:
for x being object holds
( x in dom g iff x in union (rng G) )
proof
let x be
object ;
( x in dom g iff x in union (rng G) )
hereby ( x in union (rng G) implies x in dom g )
assume
x in dom g
;
x in union (rng G)then A12:
(
x in dom (T ") &
(T ") . x in dom f )
by A2, FUNCT_1:11;
then consider Y being
set such that A13:
(
(T ") . x in Y &
Y in rng F )
by A7, TARSKI:def 4;
consider t being
object such that A14:
(
t in dom F &
Y = F . t )
by A13, FUNCT_1:def 3;
reconsider t =
t as
Nat by A14;
A15:
F . t in S
;
A16:
x = T . ((T ") . x)
by A12, A1, A6, FUNCT_1:35;
T . ((T ") . x) in T .: Y
by A12, A5, A13, FUNCT_1:def 6;
then
x in (.: T) . Y
by A1, A14, A15, A16, Th1;
then
x in ((.: T) | S) . Y
by A14, A15, FUNCT_1:49;
then A17:
x in G . t
by A14, FUNCT_1:13;
t in dom G
by A10, A14, A15, FUNCT_1:11;
then
G . t in rng G
by FUNCT_1:3;
hence
x in union (rng G)
by A17, TARSKI:def 4;
verum
end;
assume
x in union (rng G)
;
x in dom g
then consider Y being
set such that A18:
(
x in Y &
Y in rng G )
by TARSKI:def 4;
consider t being
object such that A19:
(
t in dom G &
Y = G . t )
by A18, FUNCT_1:def 3;
reconsider t =
t as
Nat by A19;
Y = H . (F . t)
by A19, FUNCT_1:12;
then
Y = (.: T) . (F . t)
by FUNCT_1:49;
then
Y = T .: (F . t)
by A1, Th1;
then consider z being
object such that A20:
(
z in dom T &
z in F . t &
x = T . z )
by A18, FUNCT_1:def 6;
A21:
z = (T ") . x
by A20, A1, FUNCT_1:34;
A22:
x in dom (T ")
by A6, A20, FUNCT_1:3;
t in dom F
by A19, FUNCT_1:11;
then
F . t in rng F
by FUNCT_1:3;
then
z in union (rng F)
by A20, TARSKI:def 4;
hence
x in dom g
by A21, A7, A22, A2, FUNCT_1:11;
verum
end;
for n being Nat
for x, y being Element of Y st n in dom G & x in G . n & y in G . n holds
g . x = g . y
proof
let n be
Nat;
for x, y being Element of Y st n in dom G & x in G . n & y in G . n holds
g . x = g . ylet x,
y be
Element of
Y;
( n in dom G & x in G . n & y in G . n implies g . x = g . y )
assume A23:
(
n in dom G &
x in G . n &
y in G . n )
;
g . x = g . y
then A24:
(
x in H . (F . n) &
y in H . (F . n) )
by FUNCT_1:12;
H . (F . n) = (.: T) . (F . n)
by FUNCT_1:49;
then A25:
(
x in T .: (F . n) &
y in T .: (F . n) )
by A24, A1, Th1;
then consider t being
object such that A26:
(
t in dom T &
t in F . n &
x = T . t )
by FUNCT_1:def 6;
reconsider t =
t as
Element of
X by A26;
consider s being
object such that A27:
(
s in dom T &
s in F . n &
y = T . s )
by A25, FUNCT_1:def 6;
reconsider s =
s as
Element of
X by A27;
g . x = f . ((T ") . (T . t))
by A2, A5, A6, A26, FUNCT_1:13;
then A28:
g . x = f . t
by A26, A1, FUNCT_1:34;
g . y = f . ((T ") . (T . s))
by A2, A5, A6, A27, FUNCT_1:13;
then
g . y = f . s
by A27, A1, FUNCT_1:34;
hence
g . x = g . y
by A23, A26, A27, A7, A28, FUNCT_1:11;
verum
end;
hence
g is_simple_func_in CopyField (T,S)
by A8, A11, TARSKI:2, MESFUNC2:def 4; verum