let A, B be functional set ; for A1 being Subset of A
for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
let A1 be Subset of A; for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
let B1 be Subset of B; FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
set f = (FuncComp (A,B)) | [:B1,A1:];
A1:
dom (FuncComp (A,B)) = [:B,A:]
by PARTFUN1:def 2;
then A2:
dom ((FuncComp (A,B)) | [:B1,A1:]) = [:B1,A1:]
by RELAT_1:62;
then reconsider f = (FuncComp (A,B)) | [:B1,A1:] as ManySortedFunction of [:B1,A1:] by PARTFUN1:def 2;
f is compositional
proof
let i be
object ;
ALTCAT_1:def 9 ( i in dom f implies ex f, g being Function st
( i = [g,f] & f . i = g * f ) )
assume A3:
i in dom f
;
ex f, g being Function st
( i = [g,f] & f . i = g * f )
then
f . i = (FuncComp (A,B)) . i
by FUNCT_1:49;
hence
ex
f,
g being
Function st
(
i = [g,f] &
f . i = g * f )
by A1, A2, A3, Def9;
verum
end;
hence
FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
by Def10; verum