let N, X, I be non empty set ; for v1, v2 being Function st dom v1 = dom v2 & dom v1 = Funcs (X,I) holds
for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds
v1 = v2
let v1, v2 be Function; ( dom v1 = dom v2 & dom v1 = Funcs (X,I) implies for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds
v1 = v2 )
assume that
A1:
dom v1 = dom v2
and
A2:
dom v1 = Funcs (X,I)
; for f being Function of X,N st f is one-to-one & v1 ** (f,N) = v2 ** (f,N) holds
v1 = v2
reconsider rv1 = rng v1, rv2 = rng v2 as non empty set by A1, A2, RELAT_1:42;
reconsider Z = rv1 \/ rv2 as non empty set ;
A3:
rng v2 c= Z
by XBOOLE_1:7;
rng v1 c= Z
by XBOOLE_1:7;
then reconsider f1 = v1, f2 = v2 as Element of Funcs ((Funcs (X,I)),Z) by A1, A2, A3, FUNCT_2:def 2;
let f be Function of X,N; ( f is one-to-one & v1 ** (f,N) = v2 ** (f,N) implies v1 = v2 )
assume that
A4:
f is one-to-one
and
A5:
v1 ** (f,N) = v2 ** (f,N)
; v1 = v2
A6:
dom (f2 ** (f,N)) = Funcs (N,I)
by FUNCT_2:def 1;
A7:
dom (f1 ** (f,N)) = Funcs (N,I)
by FUNCT_2:def 1;
now for a being object st a in Funcs (X,I) holds
v1 . a = v2 . aset i = the
Element of
I;
let a be
object ;
( a in Funcs (X,I) implies v1 . a = v2 . a )A8:
dom f = X
by FUNCT_2:def 1;
assume
a in Funcs (
X,
I)
;
v1 . a = v2 . athen reconsider h =
a as
Element of
Funcs (
X,
I) ;
set g =
(N --> the Element of I) +* (h * (f "));
A9:
dom h = X
by FUNCT_2:def 1;
rng (f ") = dom f
by A4, FUNCT_1:33;
then dom (h * (f ")) =
dom (f ")
by A9, RELAT_1:27
.=
rng f
by A4, FUNCT_1:33
;
then A10:
((N --> the Element of I) +* (h * (f "))) * f =
(h * (f ")) * f
by Th3
.=
h * ((f ") * f)
by RELAT_1:36
.=
h * (id X)
by A4, A8, FUNCT_1:39
.=
a
by A9, RELAT_1:52
;
(N --> the Element of I) +* (h * (f ")) is
Function of
N,
I
by A4, Th4;
then A11:
(N --> the Element of I) +* (h * (f ")) in Funcs (
N,
I)
by FUNCT_2:8;
then
(v1 ** (f,N)) . ((N --> the Element of I) +* (h * (f "))) = v1 . a
by A7, A10, Def13;
hence
v1 . a = v2 . a
by A5, A6, A11, A10, Def13;
verum end;
hence
v1 = v2
by A1, A2; verum