let I be set ; :: thesis: for A, B being ManySortedSet of
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 ; :: 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 let i be
set ;
:: 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 23;
then A3:
D . i c= C . i
by A2, PBOOLE:def 5;
A4:
F . i is
Function of
(A . i),
(B . i)
by A2, PBOOLE:def 18;
A5:
(F || C) . i is
Function of
(C . i),
(B . i)
by A2, PBOOLE:def 18;
then reconsider fc =
(F . i) | (C . i) as
Function of
(C . i),
(B . i) by A2, A4, MSAFREE:def 1;
thus ((F || C) || D) . i =
((F || C) . i) | (D . i)
by A2, A5, MSAFREE:def 1
.=
fc | (D . i)
by A2, A4, MSAFREE:def 1
.=
(F . i) | (D . i)
by A3, RELAT_1:103
.=
(F || E) . i
by A1, A2, A4, MSAFREE:def 1
;
:: thesis: verum end;
hence
(F || C) || D = F || E
by PBOOLE:3; :: thesis: verum