let i, I be set ; :: thesis: for M being ManySortedSet of
for f being Function
for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let M be ManySortedSet of ; :: thesis: for f being Function
for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let f be Function; :: thesis: for P being MSSetOp of M st P is reflexive & i in I & f = P . i holds
for x being Element of bool (M . i) holds x c= f . x
let P be MSSetOp of M; :: thesis: ( P is reflexive & i in I & f = P . i implies for x being Element of bool (M . i) holds x c= f . x )
assume that
A1: P is reflexive and
A2: i in I and
A3: f = P . i ; :: thesis: for x being Element of bool (M . i) holds x c= f . x
let x be Element of bool (M . i); :: thesis: x c= f . x
dom (([0] I) +* (i .--> x)) = I by A2, PZFMISC1:1;
then reconsider X = ([0] I) +* (i .--> x) as ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18;
A4: dom (i .--> x) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A5: X . i = (i .--> x) . i by A4, FUNCT_4:14
.= x by FUNCOP_1:87 ;
A6: X is Element of bool M by A2, Lm2, MSSUBFAM:11;
A7: i in dom P by A2, PARTFUN1:def 4;
X c= P .. X by A1, A6, Def2;
then X . i c= (P .. X) . i by A2, PBOOLE:def 5;
hence x c= f . x by A3, A5, A7, PRALG_1:def 17; :: thesis: verum