defpred S_{1}[ object ] means ex f, g being Function st

( $1 = [f,g] & f,g form_morphism_between S1,S2 );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] & S_{1}[x] ) )
from XBOOLE_0:sch 1();

take X ; :: thesis: for x being set holds

( x in X iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus for x being set holds

( x in X iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) :: thesis: verum

( $1 = [f,g] & f,g form_morphism_between S1,S2 );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] & S

take X ; :: thesis: for x being set holds

( x in X iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus for x being set holds

( x in X iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) :: thesis: verum

proof

let x be set ; :: thesis: ( x in X iff ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus ( x in X implies ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) by A1; :: thesis: ( ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) implies x in X )

given f, g being Function such that A2: x = [f,g] and

A3: f,g form_morphism_between S1,S2 ; :: thesis: x in X

( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A3, PUA2MSS1:def 12;

then A4: g in PFuncs ( the carrier' of S1, the carrier' of S2) by PARTFUN1:def 3;

( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by A3, PUA2MSS1:def 12;

then f in PFuncs ( the carrier of S1, the carrier of S2) by PARTFUN1:def 3;

then x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] by A2, A4, ZFMISC_1:87;

hence x in X by A1, A2, A3; :: thesis: verum

end;( x = [f,g] & f,g form_morphism_between S1,S2 ) )

thus ( x in X implies ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) ) by A1; :: thesis: ( ex f, g being Function st

( x = [f,g] & f,g form_morphism_between S1,S2 ) implies x in X )

given f, g being Function such that A2: x = [f,g] and

A3: f,g form_morphism_between S1,S2 ; :: thesis: x in X

( dom g = the carrier' of S1 & rng g c= the carrier' of S2 ) by A3, PUA2MSS1:def 12;

then A4: g in PFuncs ( the carrier' of S1, the carrier' of S2) by PARTFUN1:def 3;

( dom f = the carrier of S1 & rng f c= the carrier of S2 ) by A3, PUA2MSS1:def 12;

then f in PFuncs ( the carrier of S1, the carrier of S2) by PARTFUN1:def 3;

then x in [:(PFuncs ( the carrier of S1, the carrier of S2)),(PFuncs ( the carrier' of S1, the carrier' of S2)):] by A2, A4, ZFMISC_1:87;

hence x in X by A1, A2, A3; :: thesis: verum