set f = p .--> x;
A1: dom (p .--> x) = {p} by FUNCOP_1:19;
thus not p .--> x is empty ; :: thesis: p .--> x is homogeneous
let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom (p .--> x) or not y in dom (p .--> x) or len x = len y )
assume ( x in dom (p .--> x) & y in dom (p .--> x) ) ; :: thesis: len x = len y
then ( x = p & y = p ) by A1, TARSKI:def 1;
hence len x = len y ; :: thesis: verum