let I be set ; :: thesis: for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let A, B be ManySortedSet of I; :: thesis: for F being ManySortedFunction of A,B
for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let F be ManySortedFunction of A,B; :: thesis: for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let C, E be ManySortedSubset of A; :: thesis: for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E
let D be ManySortedSubset of C; :: thesis: ( E = D implies (F || C) || D = F || E )
assume A1: E = D ; :: thesis: (F || C) || D = F || E

now :: thesis: for i being object st i in I holds
((F || C) || D) . i = (F || E) . i

let i be object ; :: thesis: ( i in I implies ((F || C) || D) . i = (F || E) . i )
assume A2: i in I ; :: thesis: ((F || C) || D) . i = (F || E) . i
D c= C by PBOOLE:def 18;
then A4: D . i c= C . i by A2;
(F || C) . i is Function of (C . i),(B . i) by A2, PBOOLE:def 15;
then reconsider fc = (F . i) | (C . i) as Function of (C . i),(B . i) by A2, MSAFREE:def 1;
thus ((F || C) || D) . i = ((F || C) . i) | (D . i) by A2, MSAFREE:def 1
.= fc | (D . i) by A2, MSAFREE:def 1
.= (F . i) | (D . i) by A4, RELAT_1:74
.= (F || E) . i by A1, A2, MSAFREE:def 1 ; :: thesis: verum

end;

hence (F || C) || D = F || E ; :: thesis: verum