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;

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

hence
v1 = v2
by A1, A2; :: thesis: verumv1 . 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;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