defpred S1[ set ] means P1[$1 `1 ,$1 `2 ];
deffunc H1( set ) -> set = F5(($1 `1),($1 `2));
A3:
F2() = { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] }
proof
thus
F2()
c= { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] }
XBOOLE_0:def 10 { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } c= F2()proof
let y be
object ;
TARSKI:def 3 ( not y in F2() or y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] } )
assume
y in F2()
;
y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] }
then consider o1,
o2 being
Element of
F1()
such that A4:
y = [[o1,o2],F5(o1,o2)]
and A5:
P1[
o1,
o2]
by A1;
reconsider p =
[o1,o2] as
Element of
[:F1(),F1():] by ZFMISC_1:87;
A6:
p `1 = o1
;
p `2 = o2
;
hence
y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] }
by A4, A5, A6;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in { [o,H1(o)] where o is Element of [:F1(),F1():] : S1[o] } or y in F2() )
assume
y in { [o,F5((o `1),(o `2))] where o is Element of [:F1(),F1():] : P1[o `1 ,o `2 ] }
;
y in F2()
then consider o being
Element of
[:F1(),F1():] such that A7:
y = [o,F5((o `1),(o `2))]
and A8:
P1[
o `1 ,
o `2 ]
;
reconsider o1 =
o `1 ,
o2 =
o `2 as
Element of
F1()
by MCART_1:10;
o = [o1,o2]
by MCART_1:21;
hence
y in F2()
by A1, A7, A8;
verum
end;
reconsider x = [F3(),F4()] as Element of [:F1(),F1():] by ZFMISC_1:87;
A9:
S1[x]
by A2;
thus F2() . (F3(),F4()) =
F2() . x
.=
H1(x)
from ALTCAT_2:sch 3(A3, A9)
.=
F5(F3(),F4())
; verum