let X, Y be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let T be Function of X,Y; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
let a be FinSequence of ExtREAL ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let g be PartFunc of Y,ExtREAL; :: thesis:
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: F,a are_Re-presentation_of f ; :: thesis:
A4: ( dom T = X & rng T = Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
A5: rng T = dom (T ") by A1, FUNCT_1:33;
set H = (.: T) | S;
rng ((.: T) | S) = (.: T) .: S by RELAT_1:115;
then A6: rng ((.: T) | S) = CopyField (T,S) by A1, Def2;
A7: dom ((.: T) | S) = S by FUNCT_2:def 1;
then reconsider H = (.: T) | S as Function of S,(CopyField (T,S)) by A6, FUNCT_2:1;
reconsider G = H * F as Finite_Sep_Sequence of CopyField (T,S) by Th21, A1;
take G ; :: thesis:
thus G = ((.: T) | S) * F ; :: thesis:
A8: dom G = dom a by A3, A7, RELAT_1:27;
A9: for x being object holds
( x in dom g iff x in union (rng G) )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom g ; :: thesis:
then A10: ( x in dom (T ") & (T ") . x in dom f ) by A2, FUNCT_1:11;
then consider Y being set such that
A11: ( (T ") . x in Y & Y in rng F ) by A3, TARSKI:def 4;
consider t being object such that
A12: ( t in dom F & Y = F . t ) by A11, FUNCT_1:def 3;
reconsider t = t as Nat by A12;
A13: F . t in S ;
A14: x = T . ((T ") . x) by A10, A1, A5, FUNCT_1:35;
T . ((T ") . x) in T .: Y by A10, A4, A11, FUNCT_1:def 6;
then x in (.: T) . Y by A1, A12, A13, A14, Th1;
then x in H . Y by A12, A13, FUNCT_1:49;
then A15: x in G . t by A12, FUNCT_1:13;
t in dom G by A7, A12, A13, FUNCT_1:11;
then G . t in rng G by FUNCT_1:3;
hence x in union (rng G) by A15, TARSKI:def 4; :: thesis:

end;

assume x in union (rng G) ; :: thesis:
then consider Y being set such that
A16: ( x in Y & Y in rng G ) by TARSKI:def 4;
consider t being object such that
A17: ( t in dom G & Y = G . t ) by A16, FUNCT_1:def 3;
reconsider t = t as Nat by A17;
Y = H . (F . t) by A17, 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
A18: ( z in dom T & z in F . t & x = T . z ) by A16, FUNCT_1:def 6;
A19: z = (T ") . x by A18, A1, FUNCT_1:34;
A20: x in dom (T ") by A5, A18, FUNCT_1:3;
( t in dom F & F . t in dom H ) by A17, FUNCT_1:11;
then F . t in rng F by FUNCT_1:3;
then z in union (rng F) by A18, TARSKI:def 4;
hence x in dom g by A19, A3, A20, A2, FUNCT_1:11; :: thesis:

end;

for n being Nat st n in dom G holds
for x being object st x in G . n holds
g . x = a . n

proof

let n be Nat; :: thesis:
assume A21: n in dom G ; :: thesis:
let x be object ; :: thesis:
assume x in G . n ; :: thesis:
then A22: x in H . (F . n) by FUNCT_1:12, A21;
H . (F . n) = (.: T) . (F . n) by FUNCT_1:49;
then H . (F . n) = T .: (F . n) by A1, Th1;
then consider t being object such that
A23: ( t in dom T & t in F . n & x = T . t ) by A22, FUNCT_1:def 6;
reconsider t = t as Element of X by A23;
g . x = f . ((T ") . (T . t)) by A2, A4, A5, A23, FUNCT_1:13;
then g . x = f . t by A23, A1, FUNCT_1:34;
hence g . x = a . n by A23, A3, A8, A21; :: thesis:

end;

hence G,a are_Re-presentation_of g by A9, A3, A7, RELAT_1:27, TARSKI:2; :: thesis: