let A, B be functional set ; :: thesis: 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; :: thesis: for B1 being Subset of B holds FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
let B1 be Subset of B; :: thesis: 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 ; :: according to ALTCAT_1:def 9 :: thesis: ( i in dom f implies ex f, g being Function st
( i = [g,f] & f . i = g * f ) )
assume A3: i in dom f ; :: thesis: 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; :: thesis: verum

end;

hence FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:] by Def10; :: thesis: verum