let A, B be non empty set ; for C, y being set
for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
let C, y be set ; for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
let f be Function; ( f in Funcs (A,(Funcs (B,C))) & y in B implies ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C ) )
assume that
A1:
f in Funcs (A,(Funcs (B,C)))
and
A2:
y in B
; ( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
set cf = commute f;
commute f in Funcs (B,(Funcs (A,C)))
by A1, FUNCT_6:55;
then A3:
ex g being Function st
( g = commute f & dom g = B & rng g c= Funcs (A,C) )
by FUNCT_2:def 2;
then
(commute f) . y in rng (commute f)
by A2, FUNCT_1:def 3;
then
ex t being Function st
( t = (commute f) . y & dom t = A & rng t c= C )
by A3, FUNCT_2:def 2;
hence
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )
; verum