let M, P be strict prenet of R; :: thesis: ( ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) & ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) implies M = P )
assume that
A2: ex f being Function of N,R st
( M = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) and
A3: ex f being Function of N,R st
( P = N *' f & ( for i being Element of N holds f . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) ) ) ; :: thesis: M = P
consider f1 being Function of N,R such that
A4: M = N *' f1 and
A5: for i being Element of N holds f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A2;
consider f2 being Function of N,R such that
A6: P = N *' f2 and
A7: for i being Element of N holds f2 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A3;
for i being object st i in the carrier of N holds
f1 . i = f2 . i

proof

let i be object ; :: thesis: ( i in the carrier of N implies f1 . i = f2 . i )
assume i in the carrier of N ; :: thesis: f1 . i = f2 . i
then reconsider i = i as Element of N ;
f1 . i = "/\" ( { (N . k) where k is Element of N : k >= i } ,R) by A5
.= f2 . i by A7 ;
hence f1 . i = f2 . i ; :: thesis: verum

end;

hence M = P by A4, A6, FUNCT_2:12; :: thesis: verum