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 4;
then A2: dom ((FuncComp A,B) | [:B1,A1:]) = [:B1,A1:] by RELAT_1:91;
then reconsider f = (FuncComp A,B) | [:B1,A1:] as ManySortedFunction of [:B1,A1:] by PARTFUN1:def 4;
f is compositional

proof

let i be set ; :: according to ALTCAT_1:def 11 :: 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 A2, FUNCT_1:72;
hence ex f, g being Function st
( i = [g,f] & f . i = g * f ) by A1, A2, A3, Def11; :: thesis: verum

end;

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