let N, X, I be non empty set ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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 :: thesis: for a being object st a in Funcs (X,I) holds
v1 . a = v2 . a

set i = the Element of I;
let a be object ; :: thesis: ( 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) ; :: thesis: v1 . a = v2 . a
then 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; :: thesis: verum

end;

hence v1 = v2 by A1, A2; :: thesis: verum