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() )
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() )
A5: (F1() \/ {F3()}) \ F1() = {F3()} \ F1() by XBOOLE_1:40
.= {F3()} by A2, ZFMISC_1:59 ;
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
A6: F3() in {F3()} by TARSKI:def 1;
assume for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ; :: thesis: f . F3() = F4()
hence f . F3() = F4() by A5, A6; :: thesis: verum
end;
thus ( f . F3() = F4() implies for x being set st x in (F1() \/ {F3()}) \ F1() holds
H1(x) = f . x ) by A5, TARSKI:def 1; :: thesis: verum
end;
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()}); :: 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 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()] )
then F4() = f . F3() by A4;
hence ( P1[f,F1() \/ {F3()},F2() \/ {F4()}] iff P1[f | F1(),F1(),F2()] ) by A3; :: thesis: 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()}
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()}
A9: {F4()} c= F2() \/ {F4()} by XBOOLE_1:7;
F4() in {F4()} by TARSKI:def 1;
hence H1(x) in F2() \/ {F4()} by A9; :: thesis: verum
end;
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 ; :: 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 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() ) }
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; :: thesis: 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 ; :: 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 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) ) ) }
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; :: thesis: 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; :: thesis: verum