let I be set ; :: thesis: for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
let A, B be ManySortedSet of I; :: thesis: (Funcs) (A,B) c= bool [|A,B|]
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i )
assume A1: i in I ; :: thesis: ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i
then A2: ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def 17;
(bool [|A,B|]) . i = bool ([|A,B|] . i) by A1, Def1
.= bool [:(A . i),(B . i):] by A1, PBOOLE:def 16 ;
hence ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i by A2, FRAENKEL:2; :: thesis: verum