let I be set ; for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
let A, B be ManySortedSet of I; (Funcs) (A,B) c= bool [|A,B|]
let i be object ; PBOOLE:def 2 ( not i in I or ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i )
assume A1:
i in I
; ((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; verum