set G = (1,2)->(1,?,2) g;
let x, y be FinSequence; :: according to UNIALG_1:def 1 :: thesis: ( not x in dom ((1,2)->(1,?,2) g) or not y in dom ((1,2)->(1,?,2) g) or len x = len y )
assume that
A1: x in dom ((1,2)->(1,?,2) g) and
A2: y in dom ((1,2)->(1,?,2) g) ; :: thesis: len x = len y
dom <:<*(3 proj 1),(3 proj 3)*>:> = (dom (3 proj 1)) /\ (dom (3 proj 3)) by FUNCT_6:62;
then dom <:<*(3 proj 1),(3 proj 3)*>:> = (3 -tuples_on NAT ) /\ (dom (3 proj 3)) by Th40
.= (3 -tuples_on NAT ) /\ (3 -tuples_on NAT ) by Th40
.= 3 -tuples_on NAT ;
then dom (g * <:<*(3 proj 1),(3 proj 3)*>:>) c= 3 -tuples_on NAT by RELAT_1:44;
then ( 3 = len x & 3 = len y ) by A1, A2, FINSEQ_1:def 18;
hence len x = len y ; :: thesis: verum