let R1, R2 be FinSequence-membered set ; :: thesis: ( ( for a being object holds
( a in R1 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) & ( for a being object holds
( a in R2 iff ex p, q being FinSequence st
( a = p ^ q & p in P & q in Q ) ) ) implies R1 = R2 )
defpred S₁[ object ] means ex p, q being FinSequence st
( $1 = p ^ q & p in P & q in Q );
assume that
A1: for a being object holds
( a in R1 iff S₁[a] ) and
A2: for a being object holds
( a in R2 iff S₁[a] ) ; :: thesis: R1 = R2
thus R1 = R2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum