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:65;
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

consider i being Element of I;
let a be set ; :: 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 --> i) +* (h * (f " ));
A9: dom h = X by FUNCT_2:def 1;
rng (f " ) = dom f by A4, FUNCT_1:55;
then dom (h * (f " )) = dom (f " ) by A9, RELAT_1:46
.= rng f by A4, FUNCT_1:55 ;
then A10: ((N --> i) +* (h * (f " ))) * f = (h * (f " )) * f by Th3
.= h * ((f " ) * f) by RELAT_1:55
.= h * (id X) by A4, A8, FUNCT_1:61
.= a by A9, RELAT_1:78 ;
(N --> i) +* (h * (f " )) is Function of N,I by A4, Th4;
then A11: (N --> i) +* (h * (f " )) in Funcs N,I by FUNCT_2:11;
then (v1 ** f,N) . ((N --> 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, FUNCT_1:9; :: thesis: verum