set Y1 = F2() \/ {F4()};
set X1 = F1() \/ {F3()};
deffunc H1( set ) -> object = F4();
A4:
for f being Function of (F1() \/ {F3()}),(F2() \/ {F4()}) holds
( ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) iff f . F3() = F4() )
A7:
for f being Function of (F1() \/ {F3()}),(F2() \/ {F4()}) st ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) holds
( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] )
proof
let f be
Function of
(F1() \/ {F3()}),
(F2() \/ {F4()});
( ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) implies ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] ) )
assume
for
x being
set st
x in (F1() \/ {F3()}) \ F1() holds
H1(
x)
= f . x
;
( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] )
then
F4()
= f . F3()
by A4;
hence
(
P1[
f,
F1()
\/ {F3()},
F2()
\/ {F4()}] iff
P1[
f | F1(),
F1(),
F2()] )
by A3;
verum
end;
set F2 = { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) } ;
set F1 = { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) } ;
A8:
for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) in F2() \/ {F4()}
A10:
{ f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) } c= { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) } or x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) } )
assume
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) }
;
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
then consider f being
Function of
(F1() \/ {F3()}),
(F2() \/ {F4()}) such that A11:
x = f
and A12:
P1[
f,
F1()
\/ {F3()},
F2()
\/ {F4()}]
and A13:
rng (f | F1()) c= F2()
and A14:
for
x being
set st
x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(
x)
;
f . F3()
= F4()
by A4, A14;
hence
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
by A11, A12, A13;
verum
end;
A15:
{ f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) } c= { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) } or x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) } )
assume
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
;
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) }
then consider f being
Function of
(F1() \/ {F3()}),
(F2() \/ {F4()}) such that A16:
x = f
and A17:
P1[
f,
F1()
\/ {F3()},
F2()
\/ {F4()}]
and A18:
rng (f | F1()) c= F2()
and A19:
f . F3()
= F4()
;
for
x being
set st
x in (F1() \/ {F3()}) \ F1() holds
H1(
x)
= f . x
by A4, A19;
hence
x in { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) }
by A16, A17, A18;
verum
end;
A20:
( F1() c= F1() \/ {F3()} & F2() c= F2() \/ {F4()} )
by XBOOLE_1:7;
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
f . x = H1(x) ) ) }
from STIRL2_1:sch 3(A8, A20, A1, A7);
hence
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of (F1() \/ {F3()}),(F2() \/ {F4()}) : ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) }
by A10, A15, XBOOLE_0:def 10; verum