defpred S₁[ 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₁[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

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;