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

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

hence
FuncComp (A1,B1) = (FuncComp (A,B)) | [:B1,A1:]
by Def10; :: thesis: verum
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;( 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