deffunc H1( set ) -> set = F4();
set X1 = F1() \/ {F3()};
set Y1 = F2() \/ {F4()};
A4: for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) in F2() \/ {F4()}
proof
let x be set ; :: thesis: ( x in (F1() \/ {F3()}) \ F1() implies H1(x) in F2() \/ {F4()} )
assume x in (F1() \/ {F3()}) \ F1() ; :: thesis: H1(x) in F2() \/ {F4()}
( F4() in {F4()} & {F4()} c= F2() \/ {F4()} ) by TARSKI:def 1, XBOOLE_1:7;
hence H1(x) in F2() \/ {F4()} ; :: thesis: verum
end;
A5: ( F1() c= F1() \/ {F3()} & F2() c= F2() \/ {F4()} ) by XBOOLE_1:7;
A6: 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() )
proof
let f be Function of (F1() \/ {F3()}),(F2() \/ {F4()}); :: thesis: ( ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) iff f . F3() = F4() )
A7: (F1() \/ {F3()}) \ F1() = {F3()} \ F1() by XBOOLE_1:40
.= {F3()} by A2, ZFMISC_1:67 ;
thus ( ( for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) implies f . F3() = F4() ) :: thesis: ( f . F3() = F4() implies for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x )
proof
assume A8: for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ; :: thesis: f . F3() = F4()
F3() in {F3()} by TARSKI:def 1;
hence f . F3() = F4() by A7, A8; :: thesis: verum
end;
thus ( f . F3() = F4() implies for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) by A7, TARSKI:def 1; :: thesis: verum
end;
A9: 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()}); :: thesis: ( ( 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 A10: for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ; :: thesis: ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] )
F4() = f . F3() by A6, A10;
hence ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] ) by A3; :: thesis: verum
end;
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) ) ) } ;
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() ) } ;
A11: 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(A4, A5, A1, A9);
 A12: { 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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 A13: 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) ) ) } ; :: thesis: 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() ) }
consider f being Function of (F1() \/ {F3()}),(F2() \/ {F4()}) such that
A14: ( x = f & 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 A13;
f . F3() = F4() by A6, 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 A14; :: thesis: verum
end;
{ 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 set ; :: according to TARSKI:def 3 :: thesis: ( 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 A15: 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() ) } ; :: thesis: 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) ) ) }
consider f being Function of (F1() \/ {F3()}),(F2() \/ {F4()}) such that
A16: ( x = f & P1[f,F1() \/ {F3()},F2() \/ {F4()}] & rng (f | F1()) c= F2() & f . F3() = F4() ) by A15;
for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x by A6, A16;
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; :: thesis: verum
end;
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 A11, A12, XBOOLE_0:def 10; :: thesis: verum