set Y1 = F_{2}() \/ {F_{4}()};

set X1 = F_{1}() \/ {F_{3}()};

deffunc H_{1}( set ) -> object = F_{4}();

A4: for f being Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) holds

( ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x ) iff f . F_{3}() = F_{4}() )
_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) st ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x ) holds

( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] )
_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) } ;

set F1 = { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) } ;

A8: for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) in F_{2}() \/ {F_{4}()}
_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) } c= { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }
_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) } c= { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) }
_{1}() c= F_{1}() \/ {F_{3}()} & F_{2}() c= F_{2}() \/ {F_{4}()} )
by XBOOLE_1:7;

card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) }
from STIRL2_1:sch 3(A8, A20, A1, A7);

hence card { f where f is Function of F_{1}(),F_{2}() : P_{1}[f,F_{1}(),F_{2}()] } = card { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }
by A10, A15, XBOOLE_0:def 10; :: thesis: verum

set X1 = F

deffunc H

A4: for f being Function of (F

( ( for x being set st x in (F

H

proof

A7:
for f being Function of (F
let f be Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}); :: thesis: ( ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x ) iff f . F_{3}() = F_{4}() )

A5: (F_{1}() \/ {F_{3}()}) \ F_{1}() =
{F_{3}()} \ F_{1}()
by XBOOLE_1:40

.= {F_{3}()}
by A2, ZFMISC_1:59
;

thus ( ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x ) implies f . F_{3}() = F_{4}() )
:: thesis: ( f . F_{3}() = F_{4}() implies for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x )_{3}() = F_{4}() implies for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x )
by A5, TARSKI:def 1; :: thesis: verum

end;H

A5: (F

.= {F

thus ( ( for x being set st x in (F

H

H

proof

thus
( f . F
A6:
F_{3}() in {F_{3}()}
by TARSKI:def 1;

assume for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x
; :: thesis: f . F_{3}() = F_{4}()

hence f . F_{3}() = F_{4}()
by A5, A6; :: thesis: verum

end;assume for x being set st x in (F

H

hence f . F

H

H

( P

proof

set F2 = { f where f is Function of (F
let f be Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}); :: thesis: ( ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x ) implies ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] ) )

assume for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x
; :: thesis: ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] )

then F_{4}() = f . F_{3}()
by A4;

hence ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] iff P_{1}[f | F_{1}(),F_{1}(),F_{2}()] )
by A3; :: thesis: verum

end;H

assume for x being set st x in (F

H

then F

hence ( P

set F1 = { f where f is Function of (F

f . x = H

A8: for x being set st x in (F

H

proof

A10:
{ f where f is Function of (F
let x be set ; :: thesis: ( x in (F_{1}() \/ {F_{3}()}) \ F_{1}() implies H_{1}(x) in F_{2}() \/ {F_{4}()} )

assume x in (F_{1}() \/ {F_{3}()}) \ F_{1}()
; :: thesis: H_{1}(x) in F_{2}() \/ {F_{4}()}

A9: {F_{4}()} c= F_{2}() \/ {F_{4}()}
by XBOOLE_1:7;

F_{4}() in {F_{4}()}
by TARSKI:def 1;

hence H_{1}(x) in F_{2}() \/ {F_{4}()}
by A9; :: thesis: verum

end;assume x in (F

A9: {F

F

hence H

f . x = H

proof

A15:
{ f where f is Function of (F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) } or x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) } )

assume x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) }
; :: thesis: x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }

then consider f being Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) such that

A11: x = f and

A12: P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}]
and

A13: rng (f | F_{1}()) c= F_{2}()
and

A14: for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x)
;

f . F_{3}() = F_{4}()
by A4, A14;

hence x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }
by A11, A12, A13; :: thesis: verum

end;f . x = H

assume x in { f where f is Function of (F

f . x = H

then consider f being Function of (F

A11: x = f and

A12: P

A13: rng (f | F

A14: for x being set st x in (F

f . x = H

f . F

hence x in { f where f is Function of (F

f . x = H

proof

A20:
( F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) } or x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) } )

assume x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & f . F_{3}() = F_{4}() ) }
; :: thesis: x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) }

then consider f being Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) such that

A16: x = f and

A17: P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}]
and

A18: rng (f | F_{1}()) c= F_{2}()
and

A19: f . F_{3}() = F_{4}()
;

for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

H_{1}(x) = f . x
by A4, A19;

hence x in { f where f is Function of (F_{1}() \/ {F_{3}()}),(F_{2}() \/ {F_{4}()}) : ( P_{1}[f,F_{1}() \/ {F_{3}()},F_{2}() \/ {F_{4}()}] & rng (f | F_{1}()) c= F_{2}() & ( for x being set st x in (F_{1}() \/ {F_{3}()}) \ F_{1}() holds

f . x = H_{1}(x) ) ) }
by A16, A17, A18; :: thesis: verum

end;f . x = H

assume x in { f where f is Function of (F

f . x = H

then consider f being Function of (F

A16: x = f and

A17: P

A18: rng (f | F

A19: f . F

for x being set st x in (F

H

hence x in { f where f is Function of (F

f . x = H

card { f where f is Function of F

f . x = H

hence card { f where f is Function of F