let G be non empty DTConstrStr ; :: thesis: for n, n1, n2 being String of G st n1 ==> n2 holds
( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )
let n, n1, n2 be String of G; :: thesis: ( n1 ==> n2 implies ( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n ) )
given m1, m2, m3 being String of G, s being Symbol of G such that A1: n1 = (m1 ^ <*s*>) ^ m2 and
A2: n2 = (m1 ^ m3) ^ m2 and
A3: s ==> m3 ; :: according to LANG1:def 4 :: thesis: ( n ^ n1 ==> n ^ n2 & n1 ^ n ==> n2 ^ n )
thus n ^ n1 ==> n ^ n2 :: thesis: n1 ^ n ==> n2 ^ n take m1 ; :: according to LANG1:def 4 :: thesis: ex n2, n3 being String of G ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ n2 & n2 ^ n = (m1 ^ n3) ^ n2 & s ==> n3 )
take m2 ^ n ; :: thesis: ex n3 being String of G ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ n3) ^ (m2 ^ n) & s ==> n3 )
take m3 ; :: thesis: ex s being Symbol of G st
( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 )
take s ; :: thesis: ( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 )
thus ( n1 ^ n = (m1 ^ <*s*>) ^ (m2 ^ n) & n2 ^ n = (m1 ^ m3) ^ (m2 ^ n) & s ==> m3 ) by A1, A2, A3, FINSEQ_1:32; :: thesis: verum