defpred S1[ object , object ] means ex g being Function st
( $2 = g & dom g = F2($1) & ( for x being Element of F2($1) holds g . x = F3($1,x) ) );
A1:
for o being object st o in F1() holds
ex g being object st S1[o,g]
proof
let o be
object ;
( o in F1() implies ex g being object st S1[o,g] )
assume
o in F1()
;
ex g being object st S1[o,g]
deffunc H2(
object )
-> set =
F3(
o,$1);
consider g being
Function such that A2:
(
dom g = F2(
o) & ( for
x being
object st
x in F2(
o) holds
g . x = H2(
x) ) )
from FUNCT_1:sch 3();
take
g
;
S1[o,g]
take
g
;
( g = g & dom g = F2(o) & ( for x being Element of F2(o) holds g . x = F3(o,x) ) )
thus
(
g = g &
dom g = F2(
o) )
by A2;
for x being Element of F2(o) holds g . x = F3(o,x)
thus
for
x being
Element of
F2(
o) holds
g . x = F3(
o,
x)
by A2;
verum
end;
consider f being ManySortedSet of F1() such that
A3:
for o being object st o in F1() holds
S1[o,f . o]
from PBOOLE:sch 3(A1);
f is Function-yielding
then reconsider f = f as ManySortedFunction of F1() ;
take
f
; for o being Element of F1() holds
( dom (f . o) = F2(o) & ( for x being Element of F2(o) holds (f . o) . x = F3(o,x) ) )
let o be Element of F1(); ( dom (f . o) = F2(o) & ( for x being Element of F2(o) holds (f . o) . x = F3(o,x) ) )
A4:
S1[o,f . o]
by A3;
hence
dom (f . o) = F2(o)
; for x being Element of F2(o) holds (f . o) . x = F3(o,x)
let x be Element of F2(o); (f . o) . x = F3(o,x)
thus
(f . o) . x = F3(o,x)
by A4; verum