defpred S1[ object , object ] means for f being Function of F1(),F2()
for h being Function of F3(),F4() st f = \$1 & h = \$2 holds
h | F1() = f;
set F2 = { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
;
set F1 = { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ;
A5: for f9 being object st f9 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } holds
ex g9 being object st
( g9 in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
& S1[f9,g9] )
proof
let f9 be object ; :: thesis: ( f9 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } implies ex g9 being object st
( g9 in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
& S1[f9,g9] ) )

assume f9 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ; :: thesis: ex g9 being object st
( g9 in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
& S1[f9,g9] )

then consider f being Function of F1(),F2() such that
A6: f = f9 and
A7: P1[f,F1(),F2()] ;
consider h being
Function of F3(),F4() such that
A8: ( h | F1() = f & ( for x being set st x in F3() \ F1() holds
h . x = F5(x) ) ) from STIRL2_1:sch 2(A1, A2, A3);
A9: S1[f9,h] by A6, A8;
A10: rng f c= F2() ;
P1[h,F3(),F4()] by A4, A7, A8;
then h in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by ;
hence ex g9 being object st
( g9 in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
& S1[f9,g9] ) by A9; :: thesis: verum
end;
consider ff being Function of { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } , { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
such that
A11: for x being object st x in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } holds
S1[x,ff . x] from A12: ( F4() is empty implies F3() is empty ) by A1, A2, A3;
now :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
per cases ( F4() is empty or not F4() is empty ) ;
suppose A13: F4() is empty ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

set Empty = {} ;
A14: { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) } c=
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
or x in )

assume x in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
; :: thesis:
then ex f being Function of F3(),F4() st
( f = x & P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) ;
then x = {} by A13;
hence x in by TARSKI:def 1; :: thesis: verum
end;
A15: { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } c=
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } or x in )
assume x in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ; :: thesis:
then ex f being Function of F1(),F2() st
( f = x & P1[f,F1(),F2()] ) ;
then x = {} by ;
hence x in by TARSKI:def 1; :: thesis: verum
end;
now :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
per cases ( P1[ {} , {} , {} ] or not P1[ {} , {} , {} ] ) ;
suppose A16: P1[ {} , {} , {} ] ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

A17: rng {} = {} ;
A18: F2() is empty by ;
{} is Function of F1(),F2() by ;
then {} in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } by A3, A16, A18;
then A19: { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = by ;
A20: rng {} = {} ;
reconsider Empty = {} as Function of F3(),F4() by ;
A21: for x being set st x in F3() \ F1() holds
Empty . x = F5(x) by A12;
rng (Empty | F1()) c= F2() ;
then {} in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by A12, A13, A16, A21;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by ; :: thesis: verum
end;
suppose A22: P1[ {} , {} , {} ] ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

A23: not {} in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] }
proof
assume {} in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ; :: thesis: contradiction
then ex f being Function of F1(),F2() st
( f = {} & P1[f,F1(),F2()] ) ;
hence contradiction by A2, A3, A13, A22; :: thesis: verum
end;
A24: ( { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) } = {} or { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
= ) by ;
A25: not {} in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
proof
assume {} in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
then ex f being Function of F3(),F4() st
( f = {} & P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) ;
hence contradiction by A12, A13, A22; :: thesis: verum
end;
( { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = {} or { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = ) by ;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by ; :: thesis: verum
end;
end;
end;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
; :: thesis: verum
end;
suppose A26: not F4() is empty ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

now :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
per cases ( { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
} is empty or not { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
is empty ) ;
suppose A27: { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) } is empty ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

{ f where f is Function of F1(),F2() : P1[f,F1(),F2()] } is empty
proof
assume not { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } is empty ; :: thesis: contradiction
then consider x being object such that
A28: x in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ;
consider f being Function of F1(),F2() such that
f = x and
A29: P1[f,F1(),F2()] by A28;
A30: rng f c= F2() ;
consider h being Function of F3(),F4() such that
A31: ( h | F1() = f & ( for x being set st x in F3() \ F1() holds
h . x = F5(x) ) ) from STIRL2_1:sch 2(A1, A2, A3);
P1[h,F3(),F4()] by A4, A29, A31;
then h in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by ;
hence contradiction by A27; :: thesis: verum
end;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by A27; :: thesis: verum
end;
suppose A32: not { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) } is empty ; :: thesis: card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}

{ f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) } c= rng ff
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
or y in rng ff )

assume y in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
; :: thesis: y in rng ff
then consider f being Function of F3(),F4() such that
A33: f = y and
A34: P1[f,F3(),F4()] and
A35: rng (f | F1()) c= F2() and
A36: for x being set st x in F3() \ F1() holds
f . x = F5(x) ;
A37: dom (f | F1()) = (dom f) /\ F1() by RELAT_1:61;
dom f = F3() by ;
then A38: dom (f | F1()) = F1() by ;
then reconsider h = f | F1() as Function of F1(),(rng (f | F1())) by FUNCT_2:1;
( rng (f | F1()) is empty implies F1() is empty ) by ;
then reconsider h = h as Function of F1(),F2() by ;
P1[f | F1(),F1(),F2()] by A4, A34, A36;
then A39: h in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } ;
A40: dom ff = { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } by ;
then ff . h in rng ff by ;
then ff . h in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
;
then consider ffh being Function of F3(),F4() such that
A41: ffh = ff . h and
P1[ffh,F3(),F4()] and
rng (ffh | F1()) c= F2() and
A42: for x being set st x in F3() \ F1() holds
ffh . x = F5(x) ;
now :: thesis: for x being object st x in F3() holds
ffh . x = f . x
let x be object ; :: thesis: ( x in F3() implies ffh . x = f . x )
assume A43: x in F3() ; :: thesis: ffh . x = f . x
now :: thesis: ffh . x = f . x
per cases ( x in F1() or not x in F1() ) ;
suppose x in F1() ; :: thesis: ffh . x = f . x
then A44: x in dom h by ;
ffh | F1() = h by ;
then h . x = ffh . x by ;
hence ffh . x = f . x by ; :: thesis: verum
end;
suppose not x in F1() ; :: thesis: ffh . x = f . x
then A45: x in F3() \ F1() by ;
then ffh . x = F5(x) by A42;
hence ffh . x = f . x by ; :: thesis: verum
end;
end;
end;
hence ffh . x = f . x ; :: thesis: verum
end;
then ffh = f by FUNCT_2:12;
hence y in rng ff by ; :: thesis: verum
end;
then A46: rng ff = { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
;
for x1, x2 being object st x1 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } & x2 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } & ff . x1 = ff . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } & x2 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } & ff . x1 = ff . x2 implies x1 = x2 )
assume that
A47: x1 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } and
A48: x2 in { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } and
A49: ff . x1 = ff . x2 ; :: thesis: x1 = x2
A50: ex f2 being Function of F1(),F2() st
( x2 = f2 & P1[f2,F1(),F2()] ) by A48;
dom ff = { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } by ;
then ff . x1 in rng ff by ;
then ff . x1 in { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
;
then consider F1 being Function of F3(),F4() such that
A51: ff . x1 = F1 and
P1[F1,F3(),F4()] and
rng (F1 | F1()) c= F2() and
for x being set st x in F3() \ F1() holds
F1 . x = F5(x) ;
consider f1 being Function of F1(),F2() such that
A52: x1 = f1 and
P1[f1,F1(),F2()] by A47;
F1 | F1() = f1 by A11, A47, A52, A51;
hence x1 = x2 by A11, A48, A49, A52, A50, A51; :: thesis: verum
end;
then A53: ff is one-to-one by ;
dom ff = { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } by ;
then { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } , { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
are_equipotent by ;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
by CARD_1:5; :: thesis: verum
end;
end;
end;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
; :: thesis: verum
end;
end;
end;
hence card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) )
}
; :: thesis: verum