defpred S1[ object , object ] means for s being SortSymbol of F1() st $1 in FreeGen (s,F2()) holds
P1[s,$2,$1];
A5: FreeMSA F2() = MSAlgebra(# (FreeSort F2()),(FreeOper F2()) #) by MSAFREE:def 14;
then reconsider f1 = F4(), f2 = F5() as ManySortedFunction of FreeSort F2(), the Sorts of F3() ;
A6: for x being object st x in Union (FreeGen F2()) holds
ex y being object st
( y in Union the Sorts of F3() & S1[x,y] )
proof
let e be object ; :: thesis: ( e in Union (FreeGen F2()) implies ex y being object st
( y in Union the Sorts of F3() & S1[e,y] ) )
A7: dom the Sorts of F3() = the carrier of F1() by PARTFUN1:def 2;
assume e in Union (FreeGen F2()) ; :: thesis: ex y being object st
( y in Union the Sorts of F3() & S1[e,y] )
then consider s being object such that
A8: s in dom (FreeGen F2()) and
A9: e in (FreeGen F2()) . s by CARD_5:2;
reconsider s = s as SortSymbol of F1() by A8, PARTFUN1:def 2;
A10: e in FreeGen (s,F2()) by A9, MSAFREE:def 16;
take u = (F4() . s) . e; :: thesis: ( u in Union the Sorts of F3() & S1[e,u] )
f1 . s is Function of ((FreeSort F2()) . s),( the Sorts of F3() . s) ;
then u in the Sorts of F3() . s by A10, FUNCT_2:5;
hence u in Union the Sorts of F3() by A7, CARD_5:2; :: thesis: S1[e,u]
let s9 be SortSymbol of F1(); :: thesis: ( e in FreeGen (s9,F2()) implies P1[s9,u,e] )
assume A11: e in FreeGen (s9,F2()) ; :: thesis: P1[s9,u,e]
then ((FreeSort F2()) . s9) /\ ((FreeSort F2()) . s) <> {} by A10, XBOOLE_0:def 4;
then (FreeSort F2()) . s9 meets (FreeSort F2()) . s by XBOOLE_0:def 7;
then s = s9 by MSAFREE:12;
hence P1[s9,u,e] by A2, A11; :: thesis: verum
end;
consider G being Function of (Union (FreeGen F2())),(Union the Sorts of F3()) such that
A12: for e being object st e in Union (FreeGen F2()) holds
S1[e,G . e] from FUNCT_2:sch 1(A6);
 deffunc H1( set ) -> Element of Union the Sorts of F3() = G /. $1;
defpred S2[ object , object ] means for o being OperSymbol of F1()
for a being Element of Args (o,F3()) st $1 = [o,a] holds
$2 = (Den (o,F3())) . a;
consider R being set such that
A13: R = { [o,a] where o is Element of the carrier' of F1(), a is Element of Args (o,F3()) : verum } ;
A14: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f1 . s) . y = H1(y)
proof
let s be SortSymbol of F1(); :: thesis: for y being set st y in FreeGen (s,F2()) holds
(f1 . s) . y = H1(y)
let y be set ; :: thesis: ( y in FreeGen (s,F2()) implies (f1 . s) . y = H1(y) )
A15: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def 2;
assume A16: y in FreeGen (s,F2()) ; :: thesis: (f1 . s) . y = H1(y)
then y in (FreeGen F2()) . s by MSAFREE:def 16;
then A17: y in Union (FreeGen F2()) by A15, CARD_5:2;
then P1[s,G . y,y] by A12, A16;
hence (f1 . s) . y = G . y by A2, A16
.= G /. y by A17, FUNCT_2:def 13 ;
:: thesis: verum
end;
A18: for x being object st x in R holds
ex y being object st
( y in Union the Sorts of F3() & S2[x,y] )
proof
let e be object ; :: thesis: ( e in R implies ex y being object st
( y in Union the Sorts of F3() & S2[e,y] ) )
assume e in R ; :: thesis: ex y being object st
( y in Union the Sorts of F3() & S2[e,y] )
then consider o being OperSymbol of F1(), a being Element of Args (o,F3()) such that
A19: e = [o,a] by A13;
reconsider u = (Den (o,F3())) . a as set ;
take u ; :: thesis: ( u in Union the Sorts of F3() & S2[e,u] )
u in union (rng the Sorts of F3()) by TARSKI:def 4;
hence u in Union the Sorts of F3() by CARD_3:def 4; :: thesis: S2[e,u]
let o9 be OperSymbol of F1(); :: thesis: for a being Element of Args (o9,F3()) st e = [o9,a] holds
u = (Den (o9,F3())) . a
let x9 be Element of Args (o9,F3()); :: thesis: ( e = [o9,x9] implies u = (Den (o9,F3())) . x9 )
assume A20: e = [o9,x9] ; :: thesis: u = (Den (o9,F3())) . x9
then o = o9 by A19, XTUPLE_0:1;
hence u = (Den (o9,F3())) . x9 by A19, A20, XTUPLE_0:1; :: thesis: verum
end;
consider H being Function of R,(Union the Sorts of F3()) such that
A21: for e being object st e in R holds
S2[e,H . e] from FUNCT_2:sch 1(A18);
 A22: for s being SortSymbol of F1()
for y being set st y in FreeGen (s,F2()) holds
(f2 . s) . y = H1(y)
proof
let s be SortSymbol of F1(); :: thesis: for y being set st y in FreeGen (s,F2()) holds
(f2 . s) . y = H1(y)
let y be set ; :: thesis: ( y in FreeGen (s,F2()) implies (f2 . s) . y = H1(y) )
A23: dom (FreeGen F2()) = the carrier of F1() by PARTFUN1:def 2;
assume A24: y in FreeGen (s,F2()) ; :: thesis: (f2 . s) . y = H1(y)
then y in (FreeGen F2()) . s by MSAFREE:def 16;
then A25: y in Union (FreeGen F2()) by A23, CARD_5:2;
then P1[s,G . y,y] by A12, A24;
hence (f2 . s) . y = G . y by A4, A24
.= G /. y by A25, FUNCT_2:def 13 ;
:: thesis: verum
end;
deffunc H2( set , set , set ) -> Element of Union the Sorts of F3() = H /. [$1,$3];
A26: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
proof
let o be OperSymbol of F1(); :: thesis: for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let ts be Element of Args (o,(FreeMSA F2())); :: thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f2) * ts holds
(f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let x be Element of (Union the Sorts of F3()) * ; :: thesis: ( x = (Flatten f2) * ts implies (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A27: x = (Flatten f2) * ts ; :: thesis: (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A28: (Flatten f2) * ts = F5() # ts by A5, Th5;
then reconsider a = x as Element of Args (o,F3()) by A27;
A29: [o,a] in R by A13;
thus (f2 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A3, A28, A27, MSUALG_3:def 7
.= H . [o,x] by A21, A29
.= H /. [o,x] by A29, FUNCT_2:def 13 ; :: thesis: verum
end;
A30: for o being OperSymbol of F1()
for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
proof
let o be OperSymbol of F1(); :: thesis: for ts being Element of Args (o,(FreeMSA F2()))
for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let ts be Element of Args (o,(FreeMSA F2())); :: thesis: for x being Element of (Union the Sorts of F3()) * st x = (Flatten f1) * ts holds
(f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
let x be Element of (Union the Sorts of F3()) * ; :: thesis: ( x = (Flatten f1) * ts implies (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x) )
assume A31: x = (Flatten f1) * ts ; :: thesis: (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = H2(o,ts,x)
A32: (Flatten f1) * ts = F4() # ts by A5, Th5;
then reconsider a = x as Element of Args (o,F3()) by A31;
A33: [o,a] in R by A13;
thus (f1 . (the_result_sort_of o)) . ((Den (o,(FreeMSA F2()))) . ts) = (Den (o,F3())) . a by A1, A32, A31, MSUALG_3:def 7
.= H . [o,x] by A21, A33
.= H /. [o,x] by A33, FUNCT_2:def 13 ; :: thesis: verum
end;
f1 = f2 from MSAFREE1:sch 2(A30, A14, A26, A22);
 hence F4() = F5() ; :: thesis: verum