reconsider k12 = k1, k22 = k2 as Element of NAT by ORDINAL1:def 13;
for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
(f | k22) /^ (k12 -' 1) = (f | k21) /^ (k11 -' 1) ;
hence ex b₁ being XFinSequence st
for k11, k21 being Element of NAT st k11 = k1 & k21 = k2 holds
b₁ = (f | k21) /^ (k11 -' 1) ; :: thesis: verum