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 . d9)) where d9 is Element of D : verum } ;
reconsider F9 = 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 F9 c= Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } ))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F9 or x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )) )
assume x in rng F9 ; :: thesis: x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } ))
then consider d9 being object such that
A3: d9 in dom F and
A4: F . d9 = x by FUNCT_1:def 3;
reconsider d9 = d9 as Element of D by A3;
consider Fd being Function such that
A5: Fd = F . d9 ;
A6: rng Fd c= union { (rng (F . d9)) where d9 is Element of D : verum }
proof
A7: rng Fd in { (rng (F . d99)) where d99 is Element of D : verum } by A5;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in rng Fd or x1 in union { (rng (F . d9)) where d9 is Element of D : verum } )
assume x1 in rng Fd ; :: thesis: x1 in union { (rng (F . d9)) where d9 is Element of D : verum }
hence x1 in union { (rng (F . d9)) where d9 is Element of D : verum } by A7, TARSKI:def 4; :: thesis: verum
end;
F . d9 in rng F by A3, FUNCT_1:def 3;
then dom Fd = DOM C by A1, A5, CARD_3:108;
hence x in Funcs ((DOM C),(union { (rng (F . d9)) where d9 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 F9 = D by PARTFUN1:def 2;
then F in Funcs (D,(Funcs ((DOM C),(union { (rng (F . d9)) where d9 is Element of D : verum } )))) by A2, FUNCT_2:def 2;
hence (F . d) . e = ((commute F) . e) . d by A8, FUNCT_6:56; :: thesis: verum