let D be non empty set ; :: thesis: for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let F be ManySortedFunction of D; :: thesis: for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
set E = union { (rng (F . d')) where d' is Element of D : verum } ;
reconsider F' = F as Function ;
let C be non empty functional with_common_domain set ; :: thesis: ( C = rng F implies for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d )
assume A1: C = rng F ; :: thesis: for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
A2: rng F' c= Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F' or x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } ) )
assume x in rng F' ; :: thesis: x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )
then consider d' being set such that
A3: d' in dom F and
A4: F . d' = x by FUNCT_1:def 5;
reconsider d' = d' as Element of D by A3, PARTFUN1:def 4;
consider Fd being Function such that
A5: Fd = F . d' ;
A6: rng Fd c= union { (rng (F . d')) where d' is Element of D : verum }

proof

A7: rng Fd in { (rng (F . d'')) where d'' is Element of D : verum } by A5;
let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng Fd or x1 in union { (rng (F . d')) where d' is Element of D : verum } )
assume x1 in rng Fd ; :: thesis: x1 in union { (rng (F . d')) where d' is Element of D : verum }
hence x1 in union { (rng (F . d')) where d' is Element of D : verum } by A7, TARSKI:def 4; :: thesis: verum

end;

F . d' in rng F by A3, FUNCT_1:def 5;
then dom Fd = DOM C by A1, A5, CARD_3:def 12;
hence x in Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } ) by A4, A5, A6, FUNCT_2:def 2; :: thesis: verum

end;

let d be Element of D; :: thesis: for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d
let e be set ; :: thesis: ( e in DOM C implies (F . d) . e = ((commute F) . e) . d )
assume A8: e in DOM C ; :: thesis: (F . d) . e = ((commute F) . e) . d
dom F' = D by PARTFUN1:def 4;
then F in Funcs D,(Funcs (DOM C),(union { (rng (F . d')) where d' is Element of D : verum } )) by A2, FUNCT_2:def 2;
hence (F . d) . e = ((commute F) . e) . d by A8, FUNCT_6:86; :: thesis: verum