let I be set ; :: thesis: for A being ManySortedSet of I
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
let A be ManySortedSet of I; :: thesis: for B being non-empty ManySortedSet of I
for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
let B be non-empty ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
let F be ManySortedFunction of A,B; :: thesis: for M1, M2 being ManySortedSubset of A st M1 c= M2 holds
(F || M2) .:.: M1 = F .:.: M1
let M1, M2 be ManySortedSubset of A; :: thesis: ( M1 c= M2 implies (F || M2) .:.: M1 = F .:.: M1 )
assume A1: M1 c= M2 ; :: thesis: (F || M2) .:.: M1 = F .:.: M1

now :: thesis: for i being object st i in I holds
((F || M2) .:.: M1) . i = (F .:.: M1) . i

let i be object ; :: thesis: ( i in I implies ((F || M2) .:.: M1) . i = (F .:.: M1) . i )
assume A2: i in I ; :: thesis: ((F || M2) .:.: M1) . i = (F .:.: M1) . i
then reconsider f = F . i as Function of (A . i),(B . i) by PBOOLE:def 15;
reconsider fm = (F || M2) . i as Function of (M2 . i),(B . i) by A2, PBOOLE:def 15;
A3: M1 . i c= M2 . i by A1, A2;
fm = f | (M2 . i) by A2, MSAFREE:def 1;
hence ((F || M2) .:.: M1) . i = (f | (M2 . i)) .: (M1 . i) by A2, PBOOLE:def 20
.= f .: (M1 . i) by A3, RELAT_1:129
.= (F .:.: M1) . i by A2, PBOOLE:def 20 ;
:: thesis: verum

end;

hence (F || M2) .:.: M1 = F .:.: M1 ; :: thesis: verum