thus
P => Q is one-to-one
:: according to FUNCT_2:def 4 :: thesis: P => Q is onto

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (A,B) or x in K435((Funcs (A,B)),(P => Q)) )

assume x in Funcs (A,B) ; :: thesis: x in K435((Funcs (A,B)),(P => Q))

then x is Element of Funcs (A,B) ;

then reconsider f = x as Function of A,B ;

dom (P => Q) = Funcs (A,B) by FUNCT_2:def 1;

then A3: ((Q ") * f) * P in dom (P => Q) by FUNCT_2:8;

(P => Q) . (((Q ") * f) * P) = (Q * (((Q ") * f) * P)) * (P ") by Def1

.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36

.= (((Q * (Q ")) * f) * P) * (P ") by RELAT_1:36

.= (((id B) * f) * P) * (P ") by FUNCT_2:61

.= (f * P) * (P ") by FUNCT_2:17

.= f * (P * (P ")) by RELAT_1:36

.= f * (id A) by FUNCT_2:61

.= f by FUNCT_2:17 ;

hence x in rng (P => Q) by A3, FUNCT_1:def 3; :: thesis: verum

proof

thus
rng (P => Q) c= Funcs (A,B)
by RELAT_1:def 19; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: Funcs (A,B) c= K435((Funcs (A,B)),(P => Q))
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom (P => Q) or not x2 in dom (P => Q) or not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 )

assume ( x1 in dom (P => Q) & x2 in dom (P => Q) ) ; :: thesis: ( not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 )

then reconsider f1 = x1, f2 = x2 as Element of Funcs (A,B) by FUNCT_2:def 1;

assume (P => Q) . x1 = (P => Q) . x2 ; :: thesis: x1 = x2

then A1: (Q * f1) * (P ") = (P => Q) . f2 by Def1

.= (Q * f2) * (P ") by Def1 ;

A2: Q * f1 = (Q * f1) * (id A) by FUNCT_2:17

.= (Q * f1) * ((P ") * P) by FUNCT_2:61

.= ((Q * f2) * (P ")) * P by A1, RELAT_1:36

.= (Q * f2) * ((P ") * P) by RELAT_1:36

.= (Q * f2) * (id A) by FUNCT_2:61

.= Q * f2 by FUNCT_2:17 ;

f1 = (id B) * f1 by FUNCT_2:17

.= ((Q ") * Q) * f1 by FUNCT_2:61

.= (Q ") * (Q * f2) by A2, RELAT_1:36

.= ((Q ") * Q) * f2 by RELAT_1:36

.= (id B) * f2 by FUNCT_2:61

.= f2 by FUNCT_2:17 ;

hence x1 = x2 ; :: thesis: verum

end;assume ( x1 in dom (P => Q) & x2 in dom (P => Q) ) ; :: thesis: ( not (P => Q) . x1 = (P => Q) . x2 or x1 = x2 )

then reconsider f1 = x1, f2 = x2 as Element of Funcs (A,B) by FUNCT_2:def 1;

assume (P => Q) . x1 = (P => Q) . x2 ; :: thesis: x1 = x2

then A1: (Q * f1) * (P ") = (P => Q) . f2 by Def1

.= (Q * f2) * (P ") by Def1 ;

A2: Q * f1 = (Q * f1) * (id A) by FUNCT_2:17

.= (Q * f1) * ((P ") * P) by FUNCT_2:61

.= ((Q * f2) * (P ")) * P by A1, RELAT_1:36

.= (Q * f2) * ((P ") * P) by RELAT_1:36

.= (Q * f2) * (id A) by FUNCT_2:61

.= Q * f2 by FUNCT_2:17 ;

f1 = (id B) * f1 by FUNCT_2:17

.= ((Q ") * Q) * f1 by FUNCT_2:61

.= (Q ") * (Q * f2) by A2, RELAT_1:36

.= ((Q ") * Q) * f2 by RELAT_1:36

.= (id B) * f2 by FUNCT_2:61

.= f2 by FUNCT_2:17 ;

hence x1 = x2 ; :: thesis: verum

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Funcs (A,B) or x in K435((Funcs (A,B)),(P => Q)) )

assume x in Funcs (A,B) ; :: thesis: x in K435((Funcs (A,B)),(P => Q))

then x is Element of Funcs (A,B) ;

then reconsider f = x as Function of A,B ;

dom (P => Q) = Funcs (A,B) by FUNCT_2:def 1;

then A3: ((Q ") * f) * P in dom (P => Q) by FUNCT_2:8;

(P => Q) . (((Q ") * f) * P) = (Q * (((Q ") * f) * P)) * (P ") by Def1

.= ((Q * ((Q ") * f)) * P) * (P ") by RELAT_1:36

.= (((Q * (Q ")) * f) * P) * (P ") by RELAT_1:36

.= (((id B) * f) * P) * (P ") by FUNCT_2:61

.= (f * P) * (P ") by FUNCT_2:17

.= f * (P * (P ")) by RELAT_1:36

.= f * (id A) by FUNCT_2:61

.= f by FUNCT_2:17 ;

hence x in rng (P => Q) by A3, FUNCT_1:def 3; :: thesis: verum