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 & ( 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
A5: ( P = N *' f2 & ( 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 set st i in the carrier of N holds
f1 . i = f2 . i

proof

let i be set ; :: 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 A4
.= f2 . i by A5 ;
hence f1 . i = f2 . i ; :: thesis: verum

end;

hence M = P by A4, A5, FUNCT_2:18; :: thesis: verum