defpred S₁[ object ] means ( ex m being non zero Element of NAT st
( m <= n & $1 = PFArt (m,k) ) or $1 = PFCrt (n,k) );
A17: for X1, X2 being Element of Fin (PFuncs (NAT,{k})) st ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object holds
( x in X2 iff S₁[x] ) ) holds
X1 = X2 from LMOD_7:sch 1();
let X1, X2 be Element of Fin (PFuncs (NAT,{k})); :: thesis: ( ( for x being object holds
( x in X1 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) & ( for x being object holds
( x in X2 iff ( ex m being non zero Element of NAT st
( m <= n & x = PFArt (m,k) ) or x = PFCrt (n,k) ) ) ) implies X1 = X2 )
assume ( ( for x being object holds
( x in X1 iff S₁[x] ) ) & ( for x being object holds
( x in X2 iff S₁[x] ) ) ) ; :: thesis: X1 = X2
hence X1 = X2 by A17; :: thesis: verum