thus
P => Q is one-to-one
FUNCT_2:def 4 P => Q is onto
thus
rng (P => Q) c= Funcs (A,B)
by RELAT_1:def 19; FUNCT_2:def 3,XBOOLE_0:def 10 Funcs (A,B) c= K435((Funcs (A,B)),(P => Q))
let x be object ; TARSKI:def 3 ( not x in Funcs (A,B) or x in K435((Funcs (A,B)),(P => Q)) )
assume
x in Funcs (A,B)
; 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; verum